test-suite/output/simpl.v


1
2
3
4
5
6
7
8
9
10
11
12
13
14

(* Simpl with patterns *)

Goal forall x, 0+x = 1+x.
intro x.
simpl (_ + x).
Show.
Undo.
simpl (_ + x) at 2.
Show.
Undo.
simpl (0 + _).
Show.
Undo.
Abort.