(* Basic_2A1: includes: drop_trans_lt *)
lemma drops_trans_skip2: ∀b1,f1,L1,L. ⬇*[b1, f1] L1 ≘ L →
∀b2,f2,I2,K2. ⬇*[b2, f2] L ≘ K2.ⓘ{I2} →
(* Basic_2A1: includes: drop_trans_lt *)
lemma drops_trans_skip2: ∀b1,f1,L1,L. ⬇*[b1, f1] L1 ≘ L →
∀b2,f2,I2,K2. ⬇*[b2, f2] L ≘ K2.ⓘ{I2} →