proposition: Lemma rxcnf_and_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_and rxcnf pol f1 f2) = mk_and xcnf pol f1 f2.
proof: Proof. intros TX AF k f1 f2 IHf1 IHf2 pol. unfold mk_and, rxcnf_and. specialize (IHf1 pol). specialize (IHf2 pol). destruct (rxcnf pol f1). destruct (rxcnf pol f2). simpl in *. subst. destruct pol ; auto. rewrite <- ror_opt_cnf_cnf. destruct (ror_cnf_opt (xcnf false f1) (xcnf false f2)). reflexivity. Qed.
imports: List Refl Bool Relation_Definitions Setoid