proposition: Lemma abs_and_pol : forall (k: kind) (f1 f2: TFormula TX AF k) pol, and_cnf_opt (xcnf pol f1) (xcnf pol f2) = xcnf pol (abs_and f1 f2 (if pol then AND else OR)).
proof: Proof. unfold abs_and; intros k f1 f2 pol. destruct (is_X f1) eqn:EQ1. - apply is_X_inv in EQ1. subst. simpl. rewrite if_same. reflexivity. - destruct (is_X f2) eqn:EQ2. + apply is_X_inv in EQ2. subst. simpl. rewrite if_same. unfold and_cnf_opt. rewrite orb_comm. reflexivity. + destruct pol ; simpl; auto. Qed.
imports: List Refl Bool Relation_Definitions Setoid