proposition: Lemma rxcnf_iff_xcnf : forall {TX : kind -> Type} {AF:Type} (k: kind) (f1 f2:TFormula TX AF k) (IHf1 : forall pol : bool, fst (rxcnf pol f1) = xcnf pol f1) (IHf2 : forall pol : bool, fst (rxcnf pol f2) = xcnf pol f2), forall pol : bool, fst (rxcnf_iff rxcnf pol f1 f2) = mk_iff xcnf pol f1 f2.
proof: Proof. intros TX AF k f1 f2 IHf1 IHf2 pol. unfold rxcnf_iff. unfold mk_iff. rewrite <- (IHf1 (negb pol)). rewrite <- (IHf1 pol). rewrite <- (IHf2 false). rewrite <- (IHf2 true). destruct (rxcnf (negb pol) f1) as [c ?]. destruct (rxcnf false f2) as [c0 ?]. destruct (rxcnf pol f1) as [c1 ?]. destruct (rxcnf true f2) as [c2 ?]. destruct (ror_cnf_opt (and_cnf_opt c c0) (and_cnf_opt c1 c2)) as [c3 l3] eqn:EQ. simpl. change c3 with (fst (c3,l3)). rewrite <- EQ. rewrite ror_opt_cnf_cnf. reflexivity. Qed.
imports: List Refl Bool Relation_Definitions Setoid