(* Basic_1: includes: csubc_drop_conf_O *)
(* Basic_2A1: includes: lsubc_drop_O1_trans *)
lemma lsubc_drops_trans_isuni: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 →
(* Basic_1: includes: csubc_drop_conf_O *)
(* Basic_2A1: includes: lsubc_drop_O1_trans *)
lemma lsubc_drops_trans_isuni: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 →