elim (frees_total L2 V) #g1 #Hg1
elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
lapply (sor_inv_sle_dx … Hg) #H0g
elim (frees_total L2 V) #g1 #Hg1
elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
lapply (sor_inv_sle_dx … Hg) #H0g