+ elim (IHV f L1) -IHV [2: /3 width=4 by lsubf_sle_div, sor_inv_sle_sn/ ]
+ elim (IHT (⫯f) (L1.ⓑ{I}V)) -IHT [2: /4 width=4 by lsubf_sle_div, lsubf_pair_nn, sor_inv_sle_dx, sor_inv_tl_dx/ ]
+ -f2V -f2T -f2 -L2 #f1T #HT #Hf1T #f1V #HV #Hf1V elim (sor_isfin_ex … f1V (⫱f1T) ??)
+ /4 width=9 by frees_fwd_isfin, frees_bind, sor_inv_sle, sle_xn_tl, isfin_tl, ex2_intro/