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