-lemma drops_conf_skip1: ∀L,L2,c2,f. ⬇*[c2, f] L ≡ L2 →
- ∀I,K1,V1,c1,f1. ⬇*[c1, f1] L ≡ K1.ⓑ{I}V1 →
- â\88\80f2. f1 â\8a\9a â\86\91f2 â\89¡ f →
- ∃∃K2,V2. L2 = K2.ⓑ{I}V2 &
- ⬇*[c2, f2] K1 ≡ K2 & ⬆*[f2] V2 ≡ V1.
-#L #L2 #c2 #f #H2 #I #K1 #V1 #c1 #f1 #H1 #f2 #Hf lapply (drops_conf … H1 … H2 … Hf) -L -Hf
+lemma drops_conf_skip1: ∀b2,f,L,L2. ⬇*[b2, f] L ≘ L2 →
+ ∀b1,f1,I1,K1. ⬇*[b1, f1] L ≘ K1.ⓘ{I1} →
+ â\88\80f2. f1 â\8a\9a ⫯f2 â\89\98 f →
+ ∃∃I2,K2. L2 = K2.ⓘ{I2} &
+ ⬇*[b2, f2] K1 ≘ K2 & ⬆*[f2] I2 ≘ I1.
+#b2 #f #L #L2 #H2 #b1 #f1 #I1 #K1 #H1 #f2 #Hf lapply (drops_conf … H1 … H2 … Hf) -L -Hf