proposition: Lemma and_cnf_opt_cnf_ff_r : forall f, and_cnf_opt f cnf_ff = cnf_ff.
proof: Proof. intros. unfold and_cnf_opt. rewrite is_cnf_ff_cnf_ff. rewrite orb_comm. reflexivity. Qed.
imports: List Refl Bool Relation_Definitions Setoid