proposition: Lemma bound_ext {ff : falsity_flag} N phi rho sigma : bounded N phi -> (forall n, n < N -> rho n = sigma n) -> (rho ⊨ phi <-> sigma ⊨ phi).
proof: Proof. induction 1 in sigma, rho |- *; cbn; intros HN; try tauto. - enough (map (eval rho) v = map (eval sigma) v) as E. now setoid_rewrite E. apply Vector.map_ext_in. intros t Ht. eapply bounded_eval_t; try apply HN. now apply H. - destruct binop; now rewrite (IHbounded1 rho sigma), (IHbounded2 rho sigma). - destruct quantop. + split; intros Hd d; eapply IHbounded. all : try apply (Hd d); intros [] Hk; cbn; auto. symmetry. all: apply HN; lia. + split; intros [d Hd]; exists d; eapply IHbounded. all : try apply Hd; intros [] Hk; cbn; auto. symmetry. all: apply HN; lia. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullCore Undecidability(Shared.ListAutomation) Vector Lia