proposition: Theorem runC : forall (m : nat) (e : Expr), getB (run m e) = true -> Tautology e.
proof: Proof. intros m e; generalize (runCorrect m e). case (run m e); auto with stalmarck. intros r b l t; case b; simpl in |- *; auto with stalmarck. intros H' H'0; discriminate. Qed.
imports: Coq(ZArith)