proposition: Theorem PA2_models_agree_FO phi M rho : first_order phi -> bounded_indi 0 phi -> M ⊨ PA2 -> (M, rho) ⊨ phi -> forall M', M' ⊨ PA2 -> M' ⊨ phi.
proof: Proof. intros F B MPA2 H M' M'PA2 rho'. eapply sat_ext_closed_FO with (sigma := empty_PA2_env _); try assumption. eapply sat_ext_closed_FO with (sigma := empty_PA2_env _) in H; try assumption. eapply sat_iff_funcfree. 5: apply H. apply M'PA2. apply MPA2. intros n. split. apply F_O. cbn. reflexivity. now apply firstorder_funcfree. Qed.
imports: PeanoNat Lia Vector Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski PA2_facts)