proposition: Lemma msp_sat_ext s s' h P : (forall n, s n = s' n) -> msp_sat s h P <-> msp_sat s' h P.
proof: Proof. induction P in s, s' |- *; intros HS; cbn. - now setoid_rewrite (sp_eval_ext _ HS). - tauto. - now rewrite (IHP1 s s'), (IHP2 s s'). - now rewrite (IHP1 s s'), (IHP2 s s'). - now rewrite (IHP1 s s'), (IHP2 s s'). - split; intros H v. all: eapply IHP; try apply (H v). all: intros []; cbn; auto. - split; intros [v H]; exists v. all: eapply IHP; try apply H. all: intros []; cbn; auto. Qed.
imports: Undecidability.FOL(Semantics.FiniteTarski.Full) Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts Syntax.BinSig) Undecidability.SeparationLogic(MSL) Undecidability.Shared(Dec) Undecidability.Synthetic.DecidabilityFacts List