proposition: Lemma closed_k_bound k s : (forall n u, n >= k -> subst s n u = s) -> bound k s.
proof: Proof. revert k. induction s; intros k H. - econstructor. specialize (H n (#(S n))). simpl in H. decide (n >= k) as [Heq | Heq]. + destruct (Nat.eqb_spec n n); [injection (H Heq)|]; lia. + lia. - econstructor; [eapply IHs1 | eapply IHs2]; intros n u Hnk; injection (H n u Hnk); congruence. - econstructor. eapply IHs. intros n u Hnk. destruct n. lia. injection (H n u). tauto. lia. Qed.
imports: Lia