| elim (sor_inv_nnx … Hg) -Hg [|*: // ] #y #Hy #H destruct
generalize in match H2; generalize in match H1; -H1 -H2 cases J -J #J [| #V ] #H1 #H2
[ elim (lsubf_inv_unit1 … H1) -H1 #x1 #Y1 #H1 #H #H0 destruct
| elim (sor_inv_nnx … Hg) -Hg [|*: // ] #y #Hy #H destruct
generalize in match H2; generalize in match H1; -H1 -H2 cases J -J #J [| #V ] #H1 #H2
[ elim (lsubf_inv_unit1 … H1) -H1 #x1 #Y1 #H1 #H #H0 destruct