proposition: Lemma or_cnf_opt_cnf_ff : forall f, or_cnf_opt cnf_ff f = f.
proof: Proof. intros f. unfold or_cnf_opt. rewrite is_cnf_tt_cnf_ff. simpl. destruct (is_cnf_tt f) eqn:EQ. - apply is_cnf_tt_inv in EQ. congruence. - destruct (is_cnf_ff f) eqn:EQ1. + apply is_cnf_ff_inv in EQ1. congruence. + reflexivity. Qed.
imports: List Refl Bool Relation_Definitions Setoid