+
+theorem fle_bind_eq: ∀L1,L2. |L1| = |L2| → ∀V1,V2. ⦃L1, V1⦄ ⊆ ⦃L2, V2⦄ →
+ ∀I2,T1,T2. ⦃L1.ⓧ, T1⦄ ⊆ ⦃L2.ⓑ{I2}V2, T2⦄ →
+ ∀p,I1. ⦃L1, ⓑ{p,I1}V1.T1⦄ ⊆ ⦃L2, ⓑ{p,I2}V2.T2⦄.
+#L1 #L2 #HL #V1 #V2
+* #n1 #m1 #f1 #g1 #Hf1 #Hg1 #H1L #Hfg1 #I2 #T1 #T2
+* #n2 #m2 #f2 #g2 #Hf2 #Hg2 #H2L #Hfg2 #p #I1
+elim (lveq_inj_length … H1L) // #H1 #H2 destruct
+elim (lveq_inj_length … H2L) // -HL -H2L #H1 #H2 destruct
+elim (sor_isfin_ex f1 (⫱f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_
+elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
+/4 width=15 by frees_bind_void, frees_bind, monotonic_sle_sor, sle_tl, ex4_4_intro/
+qed.
+