proposition: Lemma subst_subst_many s n ts u : all (map closed ts) -> subst (subst_many s (S n) ts) n u = subst_many s n (u :: ts).
proof: Proof. move=> Hts. elim: s n. - move=> x n. rewrite /subst_many. have -> : S n = n + 1 by lia. rewrite seq_app /= map_app -app_assoc /=. suff: forall k, subst (nth x (map var (seq k n) ++ (var (k+n)) :: ts) (var (k + x))) (k+n) u = nth x (map var (seq k n) ++ u :: ts) (var (k+x)) by apply. elim: n x. + move=> [|x] k /=; [by rewrite Nat.eqb_refl|]. have : k + S x > k by lia. elim: ts Hts x (k + S x). * move=> _ [|x] ? /=; case Ek: (Nat.eqb _ _); move=> /Nat.eqb_spec in Ek; by [|lia]. * move=> t ts IH /= [Ht ?] [|x] ??; [by apply: Ht|]. by apply: IH. + move=> n IH [|x] k /=. * by case Ek: (Nat.eqb _ _); move=> /Nat.eqb_spec in Ek; [lia|]. * rewrite -!Nat.add_succ_comm. by apply: IH. - move=> s IHs t IHt n /=. by rewrite IHs IHt. - move=> s IHs n /=. by rewrite IHs. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun