(6steps)
PrintForm
Definitions
discrete
jlc
Sections
Support(jlc)
Doc
At:
discrete
equality
reflexive
1
1.
T:
Type
2.
eq:
{T=
}
3.
u:
T
eq(u,u)
By:
UnfoldTopAb 2
Generated subgoal:
1
2.
eq:
{eq:(T
T
)|
x,y:T. eq(x,y)
x = y }
3.
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)
}
eq(u,u)
T)| x,y:T. eq(x,y) x = y } eq(u,u)
