(9steps)
PrintForm
Definitions
core
3
jlc
Sections
Support(jlc)
Doc
At:
discrete
equality
inc
equivalence
1
3
1
1.
T:
Type
2.
x:
{T=
}
3.
x
T
T
4.
x@0,y:T. x(x@0,y)
x@0 = y
5.
x@0:
T
6.
y:
T
7.
x(x@0,y)
8.
x@0 = y
x(y,x@0)
By:
HypBackchain
Generated subgoals:
None
About:
(9steps)
PrintForm
Definitions
core
3
jlc
Sections
Support(jlc)
Doc
}
T
T
x@0,y:T. x(x@0,y) 
x@0 = y
x(y,x@0)
