+ elim (IH … HgT1 … HL12T … HT12) // -L1 -T1 #gT2 #HgT2 #HgT21
+ lapply (frees_inv_lifts_SO (Ⓣ) … HgT2 … L2 … HUT2) [ /3 width=1 by drops_refl, drops_drop/ ] -V1 -T2
+ /5 width=6 by sor_inv_sle_dx, sle_trans, sle_tl, ex2_intro/
+ ]
+| #I #V1 #T0 #HG #HL #HU #g1 #H1 #L2 #H2 #U2 #H0 destruct
+ elim (frees_inv_flat … H1) -H1 #gV1 #gT0 #HgV1 #HgT0 #Hg1
+ elim (cpx_inv_flat1 … H0) -H0 *
+ [ #V2 #T2 #HV12 #HT12 #H destruct
+ lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V
+ lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T
+ elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21
+ elim (IH … HgT0 … HL12T … HT12) // -IH -HgT0 -HL12T -HT12 #gT2 #HgT2 #HgT21
+ elim (sor_isfin_ex gV2 gT2) /2 width=3 by frees_fwd_isfin/
+ /3 width=10 by frees_flat, monotonic_sle_sor, ex2_intro/
+ | #HU2 #H destruct -HgV1
+ lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T
+ elim (IH … HgT0 … HL12T … HU2) // -L1 -T0 -V1
+ /4 width=6 by sor_inv_sle_dx, sle_trans, ex2_intro/
+ | #HU2 #H destruct -HgT0
+ lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ -H2 #HL12V
+ elim (IH … HgV1 … HL12V … HU2) // -L1 -T0 -V1
+ /4 width=6 by sor_inv_sle_sn, sle_trans, ex2_intro/
+ | #p #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #H0 #H1 #H destruct
+ elim (frees_inv_bind … HgT0) -HgT0 #gW1 #gT1 #HgW1 #HgT1 #HgT0
+ lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V
+ lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #H2
+ lapply (sle_lexs_trans … H2 gW1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12W
+ lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T
+ lapply (lexs_inv_tl … Abst … HL12T … HW12 ?) // -HL12T #HL12T
+ elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21
+ elim (IH … HgW1 … HL12W … HW12) // -HgW1 -HL12W -HW12 #gW2 #HgW2 #HgW21