test-suite/output/set.v


1
2
3
4
5
6
7
8
9
10

Goal let x:=O+O in x=x.
intro.
set (y1:=O) in (type of x).
Show.
set (y2:=O) in (value of x) at 1.
Show.
set (y3:=O) in (value of x).
Show.
trivial.
Qed.