proposition: Lemma closed_subst_invariant: forall `{Lift T, Subst V T}, forall { _ : LiftLift}, forall { _ : SubstLift}, forall k t, closed k t -> forall j, j >= k -> forall v, subst v j t = t.
proof: Proof. intros. assert (h: shift j t = t). eapply closed_monotonic; eauto. rewrite <- h at 1. eapply subst_lift. Qed.
imports: Dblib.DblibTactics