| Some definitions of interest. |
|
int_iseg | Def {i...j} == {k:| ik & kj } |
| | Thm* i,j:. {i...j} Type |
|
le | Def AB == B<A |
| | Thm* i,j:. (ij) Prop |
|
sfa_doc_weird_def | Def Weird(x; u,v. F(u;v)) == F(F(x;0);x) |
|
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 |