proposition: Lemma or_cnf_opt_cnf_ff_r : forall f, or_cnf_opt f cnf_ff = f.
proof: Proof. unfold or_cnf_opt. intros. rewrite is_cnf_tt_cnf_ff. rewrite orb_comm. simpl. apply if_cnf_tt. Qed.
imports: List Refl Bool Relation_Definitions Setoid