proposition: Lemma closed_subst s t k : bound (S k) s -> bound k t -> bound k (subst s k t).
proof: Proof. revert k t; induction s; intros k t cls_s cls_t; simpl; inv cls_s; eauto 6 using bound, bound_gt. destruct (Nat.eqb_spec n k); eauto. econstructor. lia. Qed.
imports: Lia