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