proposition: Lemma sat_ext_closed_FO phi rho sigma : first_order phi -> bounded_indi 0 phi -> (sat rho phi <-> sat sigma phi).
proof: Proof. intros F B. apply sat_ext_bounded. - intros x H. exfalso. apply H. eapply bounded_indi_up. 2: apply B. lia. - intros x ar H. exfalso. apply H. apply funcfree_bounded_func, firstorder_funcfree, F. - intros x ar H. exfalso. apply H. apply firstorder_bounded_pred, F. Qed.
imports: Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.SOL Undecidability.SOL.Util(Subst Syntax) Arith Lia Vector