Thms sat lemmas Sections ClassicalProps(jlc) Doc

rev_implies Def P Q == Q P

Thm* A,B:Prop. (A B) Prop

About:
!abstractionimpliesallpropmember