Def LangOver(Alph) == Alph*Prop

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