test-suite/output-coqtop/ShowGoal.v


1
2
3
4
5
6
7
8
9
10
11

Lemma x: forall(i : nat), exists(j k : nat), i = j /\ j = k /\ i = k.
Proof using.
  eexists.
  eexists.
  split.
    trivial.
  split.
    trivial.
Show Goal 13 at 5.
Show Goal 13 at 7.
Show Goal 13 at 9.