proposition: Lemma closed_lift_invariant: forall `{Lift T}, forall { _ : LiftZero }, forall { _ : LiftLift }, forall { _ : LiftLiftFuse }, forall k t, closed k t -> forall j, j >= k -> forall w, lift w j t = t.
proof: Proof. induction w. eauto using lift_zero. change (S w) with (1 + w). erewrite <- lift_lift_fuse by (instantiate (1 := j); lia). rewrite IHw. eapply closed_monotonic; eauto. Qed.
imports: Arith Lia Dblib.DblibTactics