proposition: Lemma bounded_subst {ff : falsity_flag} {n phi sigma tau} : bounded n phi -> (forall k, n > k -> sigma k = tau k) -> phi[sigma] = phi[tau].
proof: Proof. induction 1 in sigma, tau |- *; cbn; intros HN; trivial. - f_equal. apply Vector.map_ext_in. intros t Ht. eapply bounded_subst_t; try apply HN. now apply H. - now rewrite (IHbounded1 sigma tau), (IHbounded2 sigma tau). - f_equal. apply IHbounded. intros [|k] Hk; cbn; trivial. unfold funcomp. rewrite HN; trivial. lia. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(Shared.ListAutomation Shared.Dec) Coq(Eqdep_dec PeanoNat) Coq.Vectors.Vector Undecidability.Shared.Libs.PSL.Vectors(Vectors) EqdepFacts