var
jlc
Sections
ClassicalProps(jlc)
Doc
Def
Discrete{T} ==
x,y:T. Dec(x = y)
is mentioned by
Thm*
Discrete{Var}
[discrete__Var]
In prior sections:
discrete
jlc
list
3
jlc
Try larger context:
ClassicalProps(jlc)
var
jlc
Sections
ClassicalProps(jlc)
Doc