proposition: Lemma or_clause_correct : forall cl cl' env, eval_opt_clause env (or_clause cl cl') <-> eval_clause env cl \/ eval_clause env cl'.
proof: Proof. intros cl; induction cl as [|a cl IHcl]. - simpl. unfold eval_clause at 2. simpl. tauto. - intros cl' env. simpl. assert (HH := add_term_correct env a cl'). assert (eval_tt env a \/ ~ eval_tt env a) by (apply no_middle_eval'). destruct (add_term a cl'); simpl in *. + rewrite IHcl. unfold eval_clause in *. rewrite !make_conj_cons in *. tauto. + unfold eval_clause in *. repeat rewrite make_conj_cons in *. tauto. Qed.
imports: List Refl Bool Relation_Definitions Setoid