proposition: Lemma bound_closed_k s k u : bound k s -> subst s k u = s.
proof: Proof. Proof with eauto. intros H; revert u; induction H; intros u; simpl. - destruct (Nat.eqb_spec n k)... lia. - rewrite IHbound1, IHbound2... - f_equal... Qed.
imports: Lia