-theorem drops_conf: ∀L1,L,c1,f1. ⬇*[c1, f1] L1 ≡ L →
- ∀L2,c2,f. ⬇*[c2, f] L1 ≡ L2 →
- ∀f2. f1 ⊚ f2 ≡ f → ⬇*[c2, f2] L ≡ L2.
-#L1 #L #c1 #f1 #H elim H -L1 -L -f1
-[ #f1 #_ #L2 #c2 #f #HL2 #f2 #Hf12 elim (drops_inv_atom1 … HL2) -c1 -HL2
+theorem drops_conf: ∀b1,f1,L1,L. ⬇*[b1, f1] L1 ≡ L →
+ ∀b2,f,L2. ⬇*[b2, f] L1 ≡ L2 →
+ ∀f2. f1 ⊚ f2 ≡ f → ⬇*[b2, f2] L ≡ L2.
+#b1 #f1 #L1 #L #H elim H -f1 -L1 -L
+[ #f1 #_ #b2 #f #L2 #HL2 #f2 #Hf12 elim (drops_inv_atom1 … HL2) -b1 -HL2