proposition: Lemma eval_cnf_and_opt : forall env x y, eval_cnf env (and_cnf_opt x y) <-> eval_cnf env (and_cnf x y).
proof: Proof. unfold and_cnf_opt. intros env x y. destruct (is_cnf_ff x) eqn:F1. { apply is_cnf_ff_inv in F1. simpl. subst. unfold and_cnf. rewrite eval_cnf_app. rewrite eval_cnf_ff. tauto. } simpl. destruct (is_cnf_ff y) eqn:F2. { apply is_cnf_ff_inv in F2. simpl. subst. unfold and_cnf. rewrite eval_cnf_app. rewrite eval_cnf_ff. tauto. } destruct (is_cnf_tt y) eqn:F3. { apply is_cnf_tt_inv in F3. subst. unfold and_cnf. rewrite eval_cnf_app. rewrite eval_cnf_tt. tauto. } tauto. Qed.
imports: List Refl Bool Relation_Definitions Setoid