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