proposition: Lemma abst_simpl_correct : forall b (f:TFormula TX AF b) pol, xcnf pol f = xcnf pol (abst_simpl f).
proof: Proof. intros b f; induction f as [| | | |? ? IHf1 f2 IHf2|? ? IHf1 f2 IHf2 |? ? IHf|? ? IHf1 ? f2 IHf2|? ? IHf1 f2 IHf2|f1 IHf1 f2 IHf2]; simpl;intros; unfold mk_and,mk_or,mk_impl, mk_iff; rewrite <- ?IHf; try (rewrite <- !IHf1; rewrite <- !IHf2); try reflexivity. - rewrite needA_all. reflexivity. - rewrite is_bool_abst_simpl. destruct (is_bool f2); auto. - rewrite is_bool_abst_simpl. destruct (is_bool f2); auto. Qed.
imports: List Refl Bool Relation_Definitions Setoid