/3 width=3 by lveq_fwd_length_plus, lveq_fwd_length_le_dx, lveq_fwd_length_le_sn, plus_to_minus_2/ qed-.
lemma lveq_fwd_abst_bind_length_le: ∀I1,I2,L1,L2,V1,n1,n2.
- L1.ⓑ{I1}V1 ≋ⓧ*[n1,n2] L2.ⓘ{I2} → |L1| ≤ |L2|.
+ L1.ⓑ[I1]V1 ≋ⓧ*[n1,n2] L2.ⓘ[I2] → |L1| ≤ |L2|.
#I1 #I2 #L1 #L2 #V1 #n1 #n2 #HL
lapply (lveq_fwd_pair_sn … HL) #H destruct
elim (lveq_fwd_length … HL) -HL >length_bind >length_bind //
qed-.
lemma lveq_fwd_bind_abst_length_le: ∀I1,I2,L1,L2,V2,n1,n2.
- L1.ⓘ{I1} ≋ⓧ*[n1,n2] L2.ⓑ{I2}V2 → |L2| ≤ |L1|.
+ L1.ⓘ[I1] ≋ⓧ*[n1,n2] L2.ⓑ[I2]V2 → |L2| ≤ |L1|.
/3 width=6 by lveq_fwd_abst_bind_length_le, lveq_sym/ qed-.
(* Inversion lemmas with length for local environments **********************)
∃∃m2. L1 ≋ ⓧ*[n1,m2] L2 & 0 = n1 & ↑m2 = n2.
#L1 #L2 #n1 #n2 #H #HL12
lapply (lveq_fwd_length_plus … H) normalize >plus_n_Sm #H0
-lapply (plus2_inv_le_sn … H0 HL12) -H0 -HL12 #H0
+lapply (plus2_le_sn_sn … H0 HL12) -H0 -HL12 #H0
elim (le_inv_S1 … H0) -H0 #m2 #_ #H0 destruct
elim (lveq_inv_void_succ_dx … H) -H /2 width=3 by ex3_intro/
qed-.