proposition: Lemma rxcnf_impl_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_impl rxcnf pol f1 f2) = mk_impl xcnf pol f1 f2.
proof: Proof. intros TX AF k f1 f2 IHf1 IHf2 pol. unfold rxcnf_impl, mk_impl, mk_or. specialize (IHf1 (negb pol)). specialize (IHf2 pol). rewrite <- IHf1. rewrite <- IHf2. destruct (rxcnf (negb pol) f1). destruct (rxcnf pol f2). simpl in *. subst. destruct pol;auto. generalize (is_cnf_tt_inv (xcnf (negb true) f1)). destruct (is_cnf_tt (xcnf (negb true) f1)). + intros H. rewrite H by auto. reflexivity. + generalize (is_cnf_ff_inv (xcnf (negb true) f1)). destruct (is_cnf_ff (xcnf (negb true) f1)). * intros H. rewrite H by auto. unfold or_cnf_opt. simpl. destruct (is_cnf_tt (xcnf true f2)) eqn:EQ;auto. -- apply is_cnf_tt_inv in EQ; auto. -- destruct (is_cnf_ff (xcnf true f2)) eqn:EQ1. ++ apply is_cnf_ff_inv in EQ1. congruence. ++ reflexivity. * rewrite <- ror_opt_cnf_cnf. destruct (ror_cnf_opt (xcnf (negb true) f1) (xcnf true f2)). intros. reflexivity. Qed.
imports: List Refl Bool Relation_Definitions Setoid