proposition: Lemma bound_subst_many s n ts : all (map closed ts) -> bound (n + length ts) s -> bound n (subst_many s n ts).
proof: Proof. move=> Hts. elim: s n. - move=> x n /boundE ? /=. have [?|?] : x < n \/ n <= x by lia. + rewrite app_nth1. { by rewrite map_length seq_length. } by rewrite map_nth seq_nth; [|constructor]. + rewrite app_nth2 map_length seq_length; [done|]. apply: (@bound_ge 0); [|lia]. apply /closed_dcl. rewrite (nth_indep _ _ (lam (var 0))); [lia|]. case: (nth_in_or_default (x - n) ts (lam # 0)). * move: Hts => /all_Forall /Forall_forall. by apply. * by move=> ->. - move=> s IHs t IHt n /boundE [/IHs ? /IHt ?]. by constructor. - move=> s IHs n /boundE /(IHs (S n)) ?. by constructor. Qed.
imports: List Relations Undecidability.L.L Undecidability.L.Util.L_facts ssreflect ssrbool ssrfun