test-suite/output/simpl.v


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

(* Simpl with patterns *)

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