proposition: Theorem ExprToPropTautology : forall e : Expr, Tautology e -> ExprToProp e.
proof: Proof. intros e H'. elim (ExprToPropF e); intros f E; elim E; intros H'1 H'2; elim H'2; intros H'3 H'4; clear H'2 E. elim (ExprToPropF2 e f); [ intros H'7 H'8; apply H'7 | idtac | idtac ]; auto with stalmarck. Qed.
imports: Coq(ZArith) Stalmarck(normalize) Coq(Classical) Stalmarck(sTactic)