-lemma drops_split_trans: ∀L1,L2,t. ⬇*[t] L1 ≡ L2 → ∀t1,t2. t1 ⊚ t2 ≡ t →
- ∃∃L. ⬇*[t1] L1 ≡ L & ⬇*[t2] L ≡ L2.
-#L1 #L2 #t #H elim H -L1 -L2 -t
-[ #t1 #t2 #H elim (after_inv_empty3 … H) -H
- /2 width=3 by ex2_intro, drops_atom/
-| #I #L1 #L2 #V #t #HL12 #IHL12 #t1 #t2 #H elim (after_inv_false3 … H) -H *
- [ #tl1 #tl2 #H1 #H2 #Ht destruct elim (IHL12 … Ht) -t
- #tl #H1 #H2
- | #tl1 #H #Ht destruct elim (IHL12 … Ht) -t
+lemma drops_split_trans: ∀L1,L2,f,c. ⬇*[c, f] L1 ≡ L2 → ∀f1,f2. f1 ⊚ f2 ≡ f →
+ ∃∃L. ⬇*[c, f1] L1 ≡ L & ⬇*[c, f2] L ≡ L2.
+#L1 #L2 #f #c #H elim H -L1 -L2 -f
+[ #f #Hc #f1 #f2 #Hf @(ex2_intro … (⋆)) @drops_atom
+ #H lapply (Hc H) -c
+ #H elim (after_inv_isid3 … Hf H) -f //
+| #I #L1 #L2 #V #f #HL12 #IHL12 #f1 #f2 #Hf elim (after_inv_xxS … Hf) -Hf *
+ [ #g1 #g2 #Hf #H1 #H2 destruct elim (IHL12 … Hf) -f
+ #L #HL1 #HL2 @(ex2_intro … (L.ⓑ{I}V)) /2 width=1 by drops_drop/
+ @drops_skip //
+ | #g1 #Hf #H destruct elim (IHL12 … Hf) -f