proposition: Lemma subst_substList x s t A: validEnv' A -> subst (substList s (S x) A) x t = substList s x (t::A).
proof: Proof. revert x;induction s;simpl;intros x cl. - decide (S x > n);simpl. decide (x>n); destruct (Nat.eqb_spec n x);try lia;try tauto. subst. now rewrite Nat.sub_diag. decide (x>n). lia. destruct (n-x) eqn: eq. lia. assert (n2=n-S x) by lia. subst n2. destruct (nth_in_or_default (n-S x) A #n). + apply cl in i. now rewrite i. + rewrite e. simpl. destruct (Nat.eqb_spec n x). lia. auto. - now rewrite IHs1,IHs2. - now rewrite IHs. Qed.