(* Note: the premise đâŠf⊠cannot be removed *)
(* Basic_2A1: includes: lsuba_drop_O1_conf *)
-lemma lsuba_drops_conf_isuni: âG,L1,L2. G âą L1 â«â L2 â
+lemma lsuba_drops_conf_isuni: âG,L1,L2. G âą L1 â«â L2 â
âb,f,K1. đâŠf⊠â â©*[b,f] L1 â K1 â
ââK2. G âą K1 â«â K2 & â©*[b,f] L2 â K2.
#G #L1 #L2 #H elim H -L1 -L2