l:Alph*. L(l) 
M(l)
Thm* Alph:Type{i}, L,M:LangOver(Alph). L = M 
Prop{i'}
Q == (P 
Q) & (P Q)
Thm* A,B:Prop. (A B) Prop
Q == Q P
Thm* A,B:Prop. (A B) Prop
| lang_eq |
Def L = M == l:Alph*. L(l) M(l)
Thm* |
| iff |
Def P Q == (P Q) & (P Q)
Thm* |
| rev_implies |
Def P Q == Q P
Thm* |
About:
 |  |  |  |  |
 |  |  |  |