proposition: Lemma eval_cnf_app : forall env x y, eval_cnf env (x+++y) <-> eval_cnf env x /\ eval_cnf env y.
proof: Proof. unfold eval_cnf. intros. rewrite make_conj_rapp. rewrite make_conj_app ; auto. tauto. Qed.
imports: List Refl Bool Relation_Definitions Setoid