proposition: Lemma or_cnf_correct : forall env f f', eval_cnf env (or_cnf f f') <-> (eval_cnf env f) \/ (eval_cnf env f').
proof: Proof. intros env f; induction f as [|a f IHf]. - unfold eval_cnf. simpl. tauto. - intros. simpl. rewrite eval_cnf_app. rewrite <- eval_cnf_cons_iff. rewrite IHf. rewrite or_clause_cnf_correct. unfold eval_clause. tauto. Qed.
imports: List Refl Bool Relation_Definitions Setoid