proposition: Lemma or_cnf_opt_correct : forall env f f', eval_cnf env (or_cnf_opt f f') <-> eval_cnf env (or_cnf f f').
proof: Proof. unfold or_cnf_opt. intros env f f'. destruct (is_cnf_tt f) eqn:TF. { simpl. apply is_cnf_tt_inv in TF. subst. rewrite or_cnf_correct. rewrite eval_cnf_tt. tauto. } destruct (is_cnf_tt f') eqn:TF'. { simpl. apply is_cnf_tt_inv in TF'. subst. rewrite or_cnf_correct. rewrite eval_cnf_tt. tauto. } { simpl. destruct (is_cnf_ff f') eqn:EQ. - apply is_cnf_ff_inv in EQ. subst. rewrite or_cnf_correct. rewrite eval_cnf_ff. tauto. - tauto. } Qed.
imports: List Refl Bool Relation_Definitions Setoid