(25steps)
PrintForm
Definitions
discrete
jlc
Sections
Support(jlc)
Doc
At:
discrete
implies
bool
equality
T:Type. Discrete{T}
(
f:(T
T
).
x,y:T. f(x,y)
x = y)
By:
UnivCD
Generated subgoal:
1
1.
T:
Type
2.
Discrete{T}
f:(T
T
).
x,y:T. f(x,y)
x = y
About:
(25steps)
PrintForm
Definitions
discrete
jlc
Sections
Support(jlc)
Doc
f:(T
T
). 
x,y:T. f(x,y) 
x = y
T:Type. Discrete{T} 
(f:(TT). x,y:T. f(x,y) x = y)
f:(TT). x,y:T. f(x,y) x = y
