proposition: Lemma lift_preserves_closed: forall `{Lift T}, @LiftLift T _ -> forall k (t : T), closed k t -> closed (S k) (shift 0 t).
proof: Proof. unfold closed. intros. change (S k) with (1 + k). rewrite <- lift_lift by lia. congruence. Qed.
imports: Arith Lia Dblib.DblibTactics