proposition: Lemma subst_up_var k x sigma : x < k -> (var x)`[iter up k sigma] = var x.
proof: Proof. induction k in x, sigma |-*. - now intros ?%PeanoNat.Nat.nlt_0_r. - intros H. destruct (Compare_dec.lt_eq_lt_dec x k) as [[| <-]|]. + cbn [iter]. rewrite iter_switch. now apply IHk. + destruct x. reflexivity. change (iter _ _ _) with (up (iter up (S x) sigma)). change (var (S x)) with ((var x)`[↑]). rewrite up_term, IHk. reflexivity. constructor. + 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