Who Cites dequiv? | |
dequiv | Def DecidableEquiv == T:TypeE:TTEquivRel(T)((_1 E _2))Top |
Thm* DecidableEquiv Type{i'} | |
top | Def Top == Void given Void |
Thm* Top Type | |
assert | Def b == if b True else False fi |
Thm* b:. b Prop | |
equiv_rel | Def EquivRel x,y:T. E(x;y) == Refl(T;x,y.E(x;y)) & (Sym x,y:T. E(x;y)) & (Trans x,y:T. E(x;y)) |
Thm* T:Type, E:(TTProp). (EquivRel x,y:T. E(x,y)) Prop | |
trans | Def Trans x,y:T. E(x;y) == a,b,c:T. E(a;b) E(b;c) E(a;c) |
Thm* T:Type, E:(TTProp). (Trans x,y:T. E(x,y)) Prop | |
sym | Def Sym x,y:T. E(x;y) == a,b:T. E(a;b) E(b;a) |
Thm* T:Type, E:(TTProp). (Sym x,y:T. E(x,y)) Prop | |
refl | Def Refl(T;x,y.E(x;y)) == a:T. E(a;a) |
Thm* T:Type, E:(TTProp). Refl(T;x,y.E(x,y)) Prop |
Syntax: | DecidableEquiv | has structure: | dequiv{i:l} |
About: