(* Properties on basic slicing **********************************************)
lemma lsuby_drop_trans_be: ∀L1,L2,d,e. L1 ⊆[d, e] L2 →
(* Properties on basic slicing **********************************************)
lemma lsuby_drop_trans_be: ∀L1,L2,d,e. L1 ⊆[d, e] L2 →