proposition: Lemma sat_ext_bounded phi rho sigma : (forall x, ~ bounded_indi x phi -> get_indi rho x = get_indi sigma x) -> (forall x ar, ~ bounded_func ar x phi -> get_func rho x ar = get_func sigma x ar) -> (forall x ar, ~ bounded_pred ar x phi -> get_pred rho x ar = get_pred sigma x ar) -> sat rho phi <-> sat sigma phi.
proof: Proof. revert rho sigma. induction phi; cbn; intros rho sigma H1 H2 H3. - reflexivity. - erewrite map_ext_in with (g := eval sigma); revgoals. intros ? H. apply sat_ext_bounded_term. intros x H4. apply H1. intros H5. apply H4. eapply Forall_in in H5. apply H5. easy. intros x ar' H4. apply H2. intros H5. apply H4. eapply Forall_in in H5. apply H5. easy. destruct p; cbn. + rewrite H3. reflexivity. cbn. lia. + reflexivity. - specialize (IHphi1 rho sigma). specialize (IHphi2 rho sigma). destruct b; cbn; setoid_rewrite IHphi1; try setoid_rewrite IHphi2; try reflexivity; clear IHphi1 IHphi2. all: firstorder. - destruct q; split. + intros H d. eapply IHphi; clear IHphi. 4: apply (H d). intros []. all: firstorder. + intros H d. eapply IHphi; clear IHphi. 4: apply (H d). intros []. all: firstorder. + intros [d H]. exists d. eapply IHphi; clear IHphi. 4: apply H. intros []. all: firstorder. + intros [d H]. exists d. eapply IHphi; clear IHphi. 4: apply H. intros []. all: firstorder. - destruct q; split. + intros H f. eapply IHphi; clear IHphi. 4: eapply (H f); trivial. 2: intros [] ar H4; cbn; destruct Nat.eq_dec as [->|]. all: firstorder. + intros H f. eapply IHphi; clear IHphi. 4: eapply (H f); trivial. 2: intros [] ar H4; cbn; destruct Nat.eq_dec as [->|]. all: firstorder. + intros [f H]. exists f. eapply IHphi; clear IHphi. 4: eapply H; trivial. 2: intros [] ar H4; cbn; destruct Nat.eq_dec as [->|]. all: firstorder. + intros [f H]. exists f. eapply IHphi; clear IHphi. 4: eapply H; trivial. 2: intros [] ar H4; cbn; destruct Nat.eq_dec as [->|]. all: firstorder. - destruct q; split. + intros H P. eapply IHphi; clear IHphi. 4: eapply (H P); trivial. 3: intros [] ar H4; cbn; destruct Nat.eq_dec as [->|]. all: firstorder. + intros H P. eapply IHphi; clear IHphi. 4: eapply (H P); trivial. 3: intros [] ar H4; cbn; destruct Nat.eq_dec as [->|]. all: firstorder. + intros [P H]. exists P. eapply IHphi; clear IHphi. 4: eapply H; trivial. 3: intros [] ar H4; cbn; destruct Nat.eq_dec as [->|]. all: firstorder. + intros [P H]. exists P. eapply IHphi; clear IHphi. 4: eapply H; trivial. 3: intros [] ar H4; cbn; destruct Nat.eq_dec as [->|]. all: firstorder. Qed.
imports: Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.SOL Undecidability.SOL.Util(Subst Syntax) Arith Lia Vector