proposition: Lemma substList_is_bound y A s: validEnv' A -> bound (y+|A|) (s) -> bound y (substList s y A).
proof: Proof. intros vA. revert y. induction s;intros y dA. - apply closed_k_bound. intros k u ge. simpl. decide (y>n). + simpl. destruct (Nat.eqb_spec n k). lia. auto. + inv dA. assert (n-y<|A|) by lia. now rewrite (vA _ (nth_In A #n H)). - inv dA. simpl. constructor;auto. - simpl. constructor. apply IHs. now inv dA. Qed.