proposition: Lemma abst_eq_correct : forall (f1 f2 : GFormula isBool) (IHf1 : forall pol : bool, xcnf pol f1 = xcnf pol (abst_form pol f1)) (IHf2 : forall pol : bool, xcnf pol f2 = xcnf pol (abst_form pol f2)) (pol : bool), xcnf pol (EQ f1 f2) = xcnf pol (abst_form pol (EQ f1 f2)).
proof: Proof. intros f1 f2 IHf1 IHf2 pol. change (xcnf pol (IFF f1 f2) = xcnf pol (abst_form pol (EQ f1 f2))). rewrite abst_iff_correct by assumption. simpl. unfold abst_iff, abst_eq. unfold abs_iff. destruct (or_is_X (abst_form (negb pol) f1) (abst_form false f2) && or_is_X (abst_form pol f1) (abst_form true f2) ) ; auto. Qed.
imports: List Refl Bool Relation_Definitions Setoid