proposition: Lemma ror_opt_cnf_cnf : forall f1 f2, fst (ror_cnf_opt f1 f2) = or_cnf_opt f1 f2.
proof: Proof. unfold ror_cnf_opt, or_cnf_opt. intros f1 f2. destruct (is_cnf_tt f1). - simpl ; auto. - simpl. destruct (is_cnf_tt f2) ; simpl ; auto. destruct (is_cnf_ff f2) eqn:EQ. + reflexivity. + apply ror_cnf_cnf. Qed.
imports: List Refl Bool Relation_Definitions Setoid