Thm* A:Type, L:LangOver(A). L-induced Equiv A*A*Prop
Thm* T:Type, as,bs:T*. (as @ bs) T*
Thm* A,B:Prop. (A B) Prop
About: