proposition: Lemma rxcnf_xcnf : forall {TX : kind -> Type} {AF:Type} (k: kind) (f:TFormula TX AF k) pol, fst (rxcnf pol f) = xcnf pol f.
proof: Proof. intros TX AF k f; induction f ; simpl ; auto; intros pol. - destruct pol; simpl ; auto. - destruct pol; simpl ; auto. - destruct pol ; simpl ; auto. - intros. rewrite ratom_cnf. reflexivity. - apply rxcnf_and_xcnf; auto. - apply rxcnf_or_xcnf; auto. - apply rxcnf_impl_xcnf; auto. - intros. rewrite mk_iff_is_bool. apply rxcnf_iff_xcnf; auto. - intros. rewrite mk_iff_is_bool. apply rxcnf_iff_xcnf; auto. Qed.
imports: List Refl Bool Relation_Definitions Setoid