lemma lreq_co_dedropable: co_dedropable_sn lreq.
@lexs_liftable_co_dedropable
-/2 width=6 by cfull_lift, ceq_lift, cfull_refl, ceq_refl/
-qed-.
+/2 width=6 by cfull_lift, ceq_lift/ qed-.
lemma lreq_co_dropable_sn: co_dropable_sn lreq.
@lexs_co_dropable_sn qed-.
∃∃L2. ⬇*[b,f] L2.ⓑ{I}V ≡ K2 & L1 ≡[f2] L2 & L1.ⓑ{I}V ≡[f] L2.ⓑ{I}V.
#f1 #K1 #K2 #HK12 #b #f #I #L1 #V #HLK1 #f2 #Hf2
elim (drops_lexs_trans_next … HK12 … HLK1 … Hf2) -f1 -K1
-/2 width=6 by cfull_lift, ceq_lift, cfull_refl, ceq_refl, ex3_intro/
-qed-.
+/2 width=6 by cfull_lift, ceq_lift, ex3_intro/ qed-.