proposition: Lemma and_cnf_opt_cnf_tt : forall f, and_cnf_opt f cnf_tt = f.
proof: Proof. intros f. unfold and_cnf_opt. simpl. rewrite orb_comm. simpl. destruct (is_cnf_ff f) eqn:EQ ; auto. apply is_cnf_ff_inv in EQ. auto. Qed.
imports: List Refl Bool Relation_Definitions Setoid