WhoCites
Definitions
discrete
jlc
Sections
Support(jlc)
Doc
Who Cites not?
not
Def
A == A
False
Thm*
A:Prop. (
A)
Prop
pi2
Def
2of(t) == t.2
Thm*
A:Type, B:(A
Type), p:(a:A
B(a)). 2of(p)
B(1of(p))
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)). 2of(p) B(1of(p))A == A FalseA:Prop. (A) PropA:Type, B:(AType), p:(a:AB(a)). 2of(p) B(1of(p))
