proposition: Theorem stalmarckCorrect : forall (e : Expr) (S : State), match makeTriplets (norm e) with | tRC l s n => stalmarckP (addEq (s, rZFalse) nil) l S -> contradictory S -> Tautology e end.
proof: Proof. intros e S; generalize (refl_equal (makeTriplets (norm e))); pattern (makeTriplets (norm e)) at -2 in |- *; case (makeTriplets (norm e)). intros l r r0 H' H'0 H'1. apply <- (TautoRTauto e). apply <- (rTautotTauto (norm e)). red. rewrite <- H'; auto with stalmarck. apply stalmarckGivesValidEquation with (S := S); auto with stalmarck. Qed.