#b1 #b2 #f #L1 #K1 #HLK1 elim HLK1 -f -L1 -K1
[ #f #_ #L2 #K2 #HLK2 #H lapply (length_inv_zero_sn … H) -H
#H destruct elim (drops_inv_atom1 … HLK2) -HLK2 //
-| #f #I1 #L1 #K1 #V1 #_ #IH #X2 #K2 #HX #H elim (length_inv_succ_sn … H) -H
- #I2 #L2 #V2 #H12 #H destruct lapply (drops_inv_drop1 … HX) -HX
+| #f #I1 #L1 #K1 #_ #IH #X2 #K2 #HX #H elim (length_inv_succ_sn … H) -H
+ #I2 #L2 #H12 #H destruct lapply (drops_inv_drop1 … HX) -HX
#HLK2 @(IH … HLK2 H12) (**) (* auto fails *)
-| #f #I1 #L1 #K1 #V1 #V2 #_ #_ #IH #X2 #Y2 #HX #H elim (length_inv_succ_sn … H) -H
- #I2 #L2 #V2 #H12 #H destruct elim (drops_inv_skip1 … HX) -HX
- #K2 #W2 #HLK2 #_ #H destruct
- lapply (IH … HLK2 H12) -f >length_pair >length_pair /2 width=1 by/ (**) (* full auto fails *)
+| #f #I1 #I2 #L1 #K1 #_ #_ #IH #X2 #Y2 #HX #H elim (length_inv_succ_sn … H) -H
+ #I2 #L2 #H12 #H destruct elim (drops_inv_skip1 … HX) -HX
+ #I2 #K2 #HLK2 #_ #H destruct
+ lapply (IH … HLK2 H12) -f >length_bind >length_bind /2 width=1 by/ (**) (* full auto fails *)
]
qed-.
∃∃n. 𝐂⦃f⦄ ≡ n & |L1| = |L2| + n.
#f #L1 #L2 #H elim H -f -L1 -L2
[ /4 width=3 by fcla_isid, ex2_intro/
-| #f #I #L1 #L2 #V #_ * >length_pair /3 width=3 by fcla_next, ex2_intro, eq_f/
-| #f #I #L1 #L2 #V1 #V2 #_ #_ * >length_pair >length_pair /3 width=3 by fcla_push, ex2_intro/
+| #f #I #L1 #L2 #_ * >length_bind /3 width=3 by fcla_next, ex2_intro, eq_f/
+| #f #I1 #I2 #L1 #L2 #_ #_ * >length_bind >length_bind /3 width=3 by fcla_push, ex2_intro/
]
qed-.
#k #Hm #H <(fcla_mono … Hm … Hn) -f //
qed-.
-lemma drops_fwd_fcla_lt2: ∀f,L1,I2,K2,V2. ⬇*[Ⓣ, f] L1 ≡ K2.ⓑ{I2}V2 →
+lemma drops_fwd_fcla_lt2: ∀f,L1,I2,K2. ⬇*[Ⓣ, f] L1 ≡ K2.ⓘ{I2} →
∃∃n. 𝐂⦃f⦄ ≡ n & n < |L1|.
-#f #L1 #I2 #K2 #V2 #H elim (drops_fwd_fcla … H) -H
+#f #L1 #I2 #K2 #H elim (drops_fwd_fcla … H) -H
#n #Hf #H >H -L1 /3 width=3 by le_S_S, ex2_intro/
qed-.
(* Basic_2A1: includes: drop_fwd_length_lt2 *)
-lemma drops_fcla_fwd_lt2: ∀f,L1,I2,K2,V2,n.
- â¬\87*[â\93\89, f] L1 â\89¡ K2.â\93\91{I2}V2 → 𝐂⦃f⦄ ≡ n →
+lemma drops_fcla_fwd_lt2: ∀f,L1,I2,K2,n.
+ â¬\87*[â\93\89, f] L1 â\89¡ K2.â\93\98{I2} → 𝐂⦃f⦄ ≡ n →
n < |L1|.
-#f #L1 #I2 #K2 #V2 #n #H #Hn elim (drops_fwd_fcla_lt2 … H) -H
+#f #L1 #I2 #K2 #n #H #Hn elim (drops_fwd_fcla_lt2 … H) -H
#k #Hm #H <(fcla_mono … Hm … Hn) -f //
qed-.