bs ; a.as' a.(as' @ bs) (recursive)
Thm* 
T:Type, as,bs:T*. (as @ bs) 
T*
Q == (P 
Q) & (P Q)
Thm* A,B:Prop. (A B) Prop
Q == Q P
Thm* A,B:Prop. (A B) Prop
| append |
Def as @ bs == Case of as; nil bs ; a.as' a.(as' @ bs) (recursive)
Thm* |
| iff |
Def P Q == (P Q) & (P Q)
Thm* |
| rev_implies |
Def P Q == Q P
Thm* |
About:
 |  |  |  |  |  |
 |  |  |  |  |