(6steps)
PrintForm
Definitions
discrete
jlc
Sections
Support(jlc)
Doc
At:
discrete
equality
reflexive
1
1
1.
T:
Type
2.
eq:
{eq:(T
T
)|
x,y:T. eq(x,y)
x = y }
3.
u:
T
eq(u,u)
By:
Analyze 2
Generated subgoal:
1
2.
eq:
T
T
3.
x,y:T. eq(x,y)
x = y
4.
u:
T
eq(u,u)
About:
(6steps)
PrintForm
Definitions
discrete
jlc
Sections
Support(jlc)
Doc
T
x,y:T. eq(x,y) 
x = y
eq(u,u)T)| x,y:T. eq(x,y) x = y }
eq(u,u)
Tx,y:T. eq(x,y) x = y eq(u,u)
