WhoCites
Definitions
discrete
jlc
Sections
Support(jlc)
Doc
Who Cites not?
not
Def
A == A
False
Thm*
A:Prop. (
A)
Prop
pi1
Def
1of(t) == t.1
Thm*
A:Type, B:(A
Type), p:(a:A
B(a)). 1of(p)
A
About:
WhoCites
Definitions
discrete
jlc
Sections
Support(jlc)
Doc
A == A 
False
A:Prop. (A) 
PropA:Type, B:(A
Type), p:(a:A
B(a)). 1of(p) AA == A FalseA:Prop. (A) PropA:Type, B:(AType), p:(a:AB(a)). 1of(p) A
