proposition: Lemma sat_ext rho1 rho2 phi : rho1 ≡ rho2 -> sat rho1 phi <-> sat rho2 phi.
proof: Proof. revert rho1 rho2. induction phi; cbn; intros rho1 rho2 H. - easy. - destruct p. + rename t into v. enough (map (eval rho1) v = map (eval rho2) v) as <- by apply H. apply map_ext. induction v; firstorder. apply eval_ext; apply H. + rename t into v. enough (map (eval rho1) v = map (eval rho2) v) as <- by easy. apply map_ext. induction v; firstorder. apply eval_ext; apply H. - specialize (IHphi1 rho1 rho2); specialize (IHphi2 rho1 rho2). destruct b; cbn; tauto. - destruct q; split; cbn. + intros H1 x. eapply IHphi. 2: apply H1. now apply env_equiv_symm, env_equiv_cons_i. + intros H1 x. eapply IHphi. 2: apply H1. now apply env_equiv_cons_i. + intros [d H1]. exists d. eapply IHphi. 2: apply H1. now apply env_equiv_symm, env_equiv_cons_i. + intros [d H1]. exists d. eapply IHphi. 2: apply H1. now apply env_equiv_cons_i. - destruct q; split; cbn. + intros H1 f. eapply IHphi. 2: apply H1. now apply env_equiv_symm, env_equiv_cons_f. + intros H1 f. eapply IHphi. 2: apply H1. now apply env_equiv_cons_f. + intros [f H1]. exists f. eapply IHphi. 2: apply H1. now apply env_equiv_symm, env_equiv_cons_f. + intros [f H1]. exists f. eapply IHphi. 2: apply H1. now apply env_equiv_cons_f. - destruct q; split; cbn. + intros H1 P. eapply IHphi. 2: apply H1. now apply env_equiv_symm, env_equiv_cons_p. + intros H1 P. eapply IHphi. 2: apply H1. now apply env_equiv_cons_p. + intros [P H1]. exists P. eapply IHphi. 2: apply H1. now apply env_equiv_symm, env_equiv_cons_p. + intros [P H1]. exists P. eapply IHphi. 2: apply H1. now apply env_equiv_cons_p. Qed.
imports: Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.SOL Undecidability.SOL.Util(Subst Syntax) Arith Lia Vector