#L1 #L2 #HL #V1 #T1 #T * #n1 #x #f1 #g #Hf1 #Hg #H1n1 #H2n1 #H #p #I
elim (fsle_frees_trans … H … Hg) -H #n2 #n #f2 #Hf2 #H1n2 #H2n2
elim (lveq_inj_void_sn_ge … H1n1 … H1n2) -H1n2 // #H1 #H2 #H3 destruct
#L1 #L2 #HL #V1 #T1 #T * #n1 #x #f1 #g #Hf1 #Hg #H1n1 #H2n1 #H #p #I
elim (fsle_frees_trans … H … Hg) -H #n2 #n #f2 #Hf2 #H1n2 #H2n2
elim (lveq_inj_void_sn_ge … H1n1 … H1n2) -H1n2 // #H1 #H2 #H3 destruct