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