| Some definitions of interest. |
|
assoced | Def a ~ b == a | b & b | a |
| | Thm* a,b:. (a ~ b) Prop |
|
equiv_rel | Def EquivRel x,y:T. E(x;y)
Def == 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 |
|
iff | Def P Q == (P Q) & (P Q) |
| | Thm* A,B:Prop. (A B) Prop |