proposition: Theorem sat_iff_funcfree rho1 rho2 phi : rho1 ≈FF rho2 -> funcfree phi -> rho1 ⊨ phi <-> rho2 ⊨ phi.
proof: Proof. Proof using M2_correct M1_correct. revert phi rho1 rho2. induction phi; intros rho1 rho2 H F; cbn. - easy. - destruct p; cbn. + apply H. induction t; cbn. easy. split. apply F_term_funcfree. apply H. apply F. apply IHt, F. + destruct P. cbn in t. revert F. apply (Vector.caseS' t). intros ? t1. apply (Vector.caseS' t1). intros ? t0. pattern t0. apply Vector.case0. cbn. intros. now apply F_eq; apply F_term_funcfree. - destruct F as [F1 F2]. specialize (IHphi1 rho1 rho2 H F1); specialize (IHphi2 rho1 rho2 H F2). destruct b; tauto. - destruct q; split. + intros H1 y. destruct (F_surjective y). eapply IHphi. 2: easy. 2: apply H1. apply iso_env_funcfree_i; eauto. + intros H1 x. destruct (F_total x). eapply IHphi. 2: easy. 2: apply H1. apply iso_env_funcfree_i; eauto. + intros [x H1]. destruct (F_total x) as [y]. exists y. eapply IHphi. 2: easy. 2: apply H1. apply iso_env_funcfree_i; eauto. + intros [y H1]. destruct (F_surjective y) as [x]. exists x. eapply IHphi. 2: easy. 2: apply H1. apply iso_env_funcfree_i; eauto. - easy. - destruct q; split. + intros H1 P2. destruct (P2_to_P1 _ P2) as [P1 H2]. eapply IHphi. 3: apply H1. apply iso_env_funcfree_p; eauto. easy. + intros H1 P1. destruct (P1_to_P2 _ P1) as [P2 H2]. eapply IHphi. 3: apply H1. apply iso_env_funcfree_p; eauto. easy. + intros [P1 H1]. destruct (P1_to_P2 _ P1) as [P2 H2]. exists P2. eapply IHphi. 3: apply H1. apply iso_env_funcfree_p; eauto. easy. + intros [P2 H1]. destruct (P2_to_P1 _ P2) as [P1 H2]. exists P1. eapply IHphi. 3: apply H1. apply iso_env_funcfree_p; eauto. easy. Qed.
imports: PeanoNat Lia Vector Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski PA2_facts)