proposition: Lemma sat_ext_closed phi rho sigma : bounded_indi 0 phi -> (forall ar, bounded_func ar 0 phi) -> (forall ar, bounded_pred ar 0 phi) -> (sat rho phi <-> sat sigma phi).
proof: Proof. intros Bi Bf Bp. apply sat_ext_bounded. - intros x H. exfalso. apply H. eapply bounded_indi_up. 2: apply Bi. lia. - intros x ar H. exfalso. apply H. eapply bounded_func_up. 2: apply Bf. lia. - intros x ar H. exfalso. apply H. eapply bounded_pred_up. 2: apply Bp. lia. Qed.
imports: Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.SOL Undecidability.SOL.Util(Subst Syntax) Arith Lia Vector