(6steps)
PrintForm
Definitions
discrete
jlc
Sections
Support(jlc)
Doc
At:
discrete
equality
properties
1
2
1.
T:
Type
2.
eq:
T
T
3.
x,y:T. eq(x,y)
x = y
(
x,y:T. eq(x,y)
x = y) & eq
T
T
By:
Auto
Generated subgoals:
1
4.
x:
T
5.
y:
T
6.
eq(x,y)
x = y
2
4.
x:
T
5.
y:
T
6.
x = y
eq(x,y)
About:
(6steps)
PrintForm
Definitions
discrete
jlc
Sections
Support(jlc)
Doc
x = y eq(x,y)
T
x,y:T. eq(x,y) 
x = y
(x,y:T. eq(x,y) x = y) & eq 
TT
x = y eq(x,y)
