proposition: Lemma many_subst_closed (s : term) {k} n (v : Vector.t term k) : closed s -> many_subst s n v = s.
proof: Proof. induction v in n, s |- *. - reflexivity. - cbn. intros H. rewrite H. now eapply IHv. Qed.
imports: Undecidability.L(LTactics) Undecidability.Shared.Libs.PSL.Vectors.Vectors Vector List