(* Basic_2A1: includes: lreq_drop_trans_be *)
lemma lreq_drops_trans_next: ∀f2,L1,L2. L1 ≡[f2] L2 →
∀b,f,I,K2. ⬇*[b, f] L2 ≘ K2.ⓘ{I} → 𝐔⦃f⦄ →
(* Basic_2A1: includes: lreq_drop_trans_be *)
lemma lreq_drops_trans_next: ∀f2,L1,L2. L1 ≡[f2] L2 →
∀b,f,I,K2. ⬇*[b, f] L2 ≘ K2.ⓘ{I} → 𝐔⦃f⦄ →