(9steps)
PrintForm
Definitions
core
3
jlc
Sections
Support(jlc)
Doc
At:
discrete
equality
inc
equivalence
1
5
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.
z:
T
8.
x(x@0,y)
9.
x(y,z)
10.
x@0 = y
11.
y = z
x(x@0,z)
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(x@0,z)