+
+lemma by_level_depth_gen: ∀M,e,d,h. d ≤ e → ⇑[d, h] ⇓[e, e-d] M = 𝛌h.M.
+#M elim M -M
+[ #i #k #e #d #h #Hde >bylevel_abst normalize >(minus_plus_minus_l … Hde)
+ elim (lt_or_eq_or_gt k (i+d)) #Hkid
+ [ >(tri_lt ???? … Hkid) >(tri_lt ???? (i+d) (i+d-k-1))
+ /5 width=1 by minus_le_minus_minus_comm, monotonic_lt_minus_l, eq_f/
+ | destruct >(tri_eq ???? …) >(tri_eq ???? …) //
+ | >(tri_gt ???? … Hkid) >(tri_gt ???? … Hkid) //
+ ]
+| #i #C #A #IHC #IHA #e #d #h #Hdeh >bylevel_abst normalize
+ lapply (IHC (e+i) (i+d) 0 ?) -IHC /2 width=1 by monotonic_le_plus_r/
+ lapply (IHA (e+i) (i+d) 0 ?) -IHA /2 width=1 by monotonic_le_plus_r/
+ /3 width=1 by eq_f3, eq_f2/
+]
+qed-.
+
+theorem by_level_depth: ∀M. ⇑⇓M = M.
+#M lapply (by_level_depth_gen M 0 0 0 ?) //
+qed.