proposition: Lemma add_term_correct : forall env t cl , eval_opt_clause env (add_term t cl) <-> eval_clause env (t::cl).
proof: Proof. intros env t cl; induction cl as [|a cl IHcl]. - simpl. case_eq (deduce (fst t) (fst t)) ; try tauto. intros t0 H. generalize (@deduce_prop _ _ _ H env). case_eq (unsat t0) ; try tauto. { intros H0 ?. generalize (@unsat_prop _ H0 env). unfold eval_clause. rewrite make_conj_cons. simpl; intros. tauto. } - simpl. case_eq (deduce (fst t) (fst a)); intros t0; [intros H|]. + generalize (@deduce_prop _ _ _ H env). case_eq (unsat t0); intros H0 H1. { generalize (@unsat_prop _ H0 env). simpl. unfold eval_clause. repeat rewrite make_conj_cons. tauto. } destruct (add_term t cl) ; simpl in * ; try tauto. { intros. unfold eval_clause in *. repeat rewrite make_conj_cons in *. tauto. } { unfold eval_clause in *. repeat rewrite make_conj_cons in *. tauto. } + destruct (add_term t cl) ; simpl in *; unfold eval_clause in * ; repeat rewrite make_conj_cons in *; tauto. Qed.
imports: List Refl Bool Relation_Definitions Setoid