elim (sor_xxn_tl … Hf1) [1,2: * |*: // ] -Hf1
#gV1 #gT1 #Hg1
[ -IHT1 #H1 #_ elim (IHV1 … HL12 … H1) -IHV1 -HL12 -H1
elim (sor_xxn_tl … Hf1) [1,2: * |*: // ] -Hf1
#gV1 #gT1 #Hg1
[ -IHT1 #H1 #_ elim (IHV1 … HL12 … H1) -IHV1 -HL12 -H1
]
| #fV1 #fT1 #f1 #I1 #L1 #V1 #T1 #_ #_ #Hf1 #IHV1 #IHT1 #I2 #L2 #V2 #n #HL12 #g1 #Hgf1
lapply (sor_tls … Hf1 n) -Hf1 <Hgf1 -Hgf1 #Hf1
elim (sor_xxn_tl … Hf1) [1,2: * |*: // ] -Hf1
#gV1 #gT1 #Hg1
[ -IHT1 #H1 #_ elim (IHV1 … HL12 … H1) -IHV1 -HL12 -H1
]
| #fV1 #fT1 #f1 #I1 #L1 #V1 #T1 #_ #_ #Hf1 #IHV1 #IHT1 #I2 #L2 #V2 #n #HL12 #g1 #Hgf1
lapply (sor_tls … Hf1 n) -Hf1 <Hgf1 -Hgf1 #Hf1
elim (sor_xxn_tl … Hf1) [1,2: * |*: // ] -Hf1
#gV1 #gT1 #Hg1
[ -IHT1 #H1 #_ elim (IHV1 … HL12 … H1) -IHV1 -HL12 -H1