PrintForm
Definitions
decidability
Sections
ClassicalProps(jlc)
Doc
At:
zero
rank
all
vars
1
2
1
1
1
1
1
2
1
1
1.
z:
Formula
2.
x:
Var
0 = 0
(
v:Var.
x
=
v
)
By:
Analyze 0
Generated subgoal:
1
3.
0 = 0
v:Var.
x
=
v
About:
v:Var. 
x
= v 0 = 0 
(v:Var. x = v) v:Var. x = v
