Def L = M == l:Alph*. L(l) M(l)

Thm* Alph:Type{i}, L,M:LangOver(Alph). L = M Prop{i'}

Def P Q == (P Q) & (P Q)

Thm* A,B:Prop. (A B) Prop

Def (L M)(l) == L(l) & M(l)

Thm* Alph:Type, M,N:LangOver(Alph). (M N) LangOver(Alph)

Def (L U M)(l) == L(l) M(l)

Thm* Alph:Type, M,N:LangOver(Alph). (M U N) LangOver(Alph)

Def LangOver(Alph) == Alph*Prop

Thm* Alph:Type{i}. LangOver(Alph) Type{i'}

Def P Q == Q P

Thm* A,B:Prop. (A B) Prop