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'}