proposition: Theorem TautoRTauto : forall e : Expr, Tautology e <-> rTautology (norm e).
proof: Proof. intros e; unfold Tautology in |- *; unfold rTautology in |- *; split. intros H' f; rewrite <- normEval; auto with stalmarck. intros H' f; rewrite normEval; auto with stalmarck. Qed.