Nuprl - Some Definitions

lang_eq	`Def L = M == l:Alph. L(l) M(l)` `Thm Alph:Type{i}, L,M:LangOver(Alph). L = M Prop{i'}`
iff	`Def P Q == (P Q) & (P Q)` `Thm* A,B:Prop. (A B) Prop`
lang_compl	`Def (L)(l) == L(l)` `Thm* Alph:Type, M:LangOver(Alph). (M) LangOver(Alph)`
languages	`Def LangOver(Alph) == AlphProp` `Thm Alph:Type{i}. LangOver(Alph) Type{i'}`
not	`Def A == A False` `Thm* A:Prop. (A) Prop`
rev_implies	`Def P Q == Q P` `Thm* A,B:Prop. (A B) Prop`

About: