proposition: Theorem rTautotTauto : forall e : rExpr, rTautology e <-> tTautology e.
proof: Proof. intros e; unfold tTautology in |- *; unfold rTautology in |- *. DCase (makeTriplets e). intros l r r0 H'; split; intros H'1. red in |- *; simpl in |- *; auto with stalmarck. intros f H'0 fZ0; simpl in |- *. rewrite fZ0; auto with stalmarck. rewrite <- (H'1 f); auto with stalmarck. apply rZEvalREvalMakeTriplets with (l := l) (n := r0); auto with stalmarck. red in |- *; auto with stalmarck. intros f fZ0. red in H'1. elim (extendEvalMakeTriplets f e l r0 r); [ intros g E; elim E; intros H'7 H'8; elim H'8; intros H'9 H'10; clear H'8 E | idtac ]; auto with stalmarck. rewrite H'10. rewrite (H'1 g); simpl in |- *; auto with stalmarck. rewrite <- equalBeforeElim with (1 := H'7); auto with stalmarck. rewrite <- equalBeforeElim with (1 := H'7); auto with stalmarck. Qed.