#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.
#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.