-[ #f #I1 #Hf #X #H1 elim (tdeq_fwd_atom1 … H1) -H1
- #I2 #H1 #Y #H2 lapply (lexs_inv_atom1 … H2) -H2
- #H2 destruct /2 width=1 by frees_atom/
-| #f #I #L1 #V1 #s1 #_ #IH #X #H1 elim (tdeq_inv_sort1 … H1) -H1
- #s2 #d #Hs1 #Hs2 #H1 #Y #H2 elim (lexs_inv_push1 … H2) -H2
- #L2 #V2 #HL12 #_ #H2 destruct /4 width=3 by frees_sort, tdeq_sort/
-| #f #I #L1 #V1 #_ #IH #X #H1 >(tdeq_inv_lref1 … H1) -H1
- #Y #H2 elim (lexs_inv_next1 … H2) -H2
- #L2 #V2 #HL12 #HV12 #H2 destruct /3 width=1 by frees_zero/
-| #f #I #L1 #V1 #i #_ #IH #X #H1 >(tdeq_inv_lref1 … H1) -H1
- #Y #H2 elim (lexs_inv_push1 … H2) -H2
- #L2 #V2 #HL12 #_ #H2 destruct /3 width=1 by frees_lref/
-| #f #I #L1 #V1 #l #_ #IH #X #H1 >(tdeq_inv_gref1 … H1) -H1
- #Y #H2 elim (lexs_inv_push1 … H2) -H2
- #L2 #V2 #HL12 #_ #H2 destruct /3 width=1 by frees_gref/
-| #f1V #f1T #f1 #p #I #L1 #V1 #T1 #_ #_ #Hf1 #IHV #IHT #X #H1 elim (tdeq_inv_pair1 … H1) -H1
- #V2 #T2 #HV12 #HT12 #H1 #L2 #HL12 destruct
- /6 width=5 by frees_bind, lexs_inv_tl, sle_lexs_trans, sor_inv_sle_dx, sor_inv_sle_sn/
-| #f1V #f1T #f1 #I #L1 #V1 #T1 #_ #_ #Hf1 #IHV #IHT #X #H1 elim (tdeq_inv_pair1 … H1) -H1
- #V2 #T2 #HV12 #HT12 #H1 #L2 #HL12 destruct
+[ #f #L1 #s1 #Hf #X #H1 #L2 #_
+ elim (tdeq_inv_sort1 … H1) -H1 #s2 #d #_ #_ #H destruct
+ /2 width=3 by frees_sort/
+| #f #i #Hf #X #H1
+ >(tdeq_inv_lref1 … H1) -X #Y #H2
+ >(lexs_inv_atom1 … H2) -Y
+ /2 width=1 by frees_atom/
+| #f #I #L1 #V1 #_ #IH #X #H1
+ >(tdeq_inv_lref1 … H1) -X #Y #H2
+ elim (lexs_inv_next1 … H2) -H2 #Z #L2 #HL12 #HZ #H destruct
+ elim (ext2_inv_pair_sn … HZ) -HZ #V2 #HV12 #H destruct
+ /3 width=1 by frees_pair/
+| #f #I #L1 #Hf #X #H1
+ >(tdeq_inv_lref1 … H1) -X #Y #H2
+ elim (lexs_inv_next1 … H2) -H2 #Z #L2 #_ #HZ #H destruct
+ >(ext2_inv_unit_sn … HZ) -Z /2 width=1 by frees_unit/
+| #f #I #L1 #i #_ #IH #X #H1
+ >(tdeq_inv_lref1 … H1) -X #Y #H2
+ elim (lexs_inv_push1 … H2) -H2 #J #L2 #HL12 #_ #H destruct
+ /3 width=1 by frees_lref/
+| #f #L1 #l #Hf #X #H1 #L2 #_
+ >(tdeq_inv_gref1 … H1) -X /2 width=1 by frees_gref/
+| #f1V #f1T #f1 #p #I #L1 #V1 #T1 #_ #_ #Hf1 #IHV #IHT #X #H1
+ elim (tdeq_inv_pair1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H1 #L2 #HL12 destruct
+ /6 width=5 by frees_bind, lexs_inv_tl, ext2_pair, sle_lexs_trans, sor_inv_sle_dx, sor_inv_sle_sn/
+| #f1V #f1T #f1 #I #L1 #V1 #T1 #_ #_ #Hf1 #IHV #IHT #X #H1
+ elim (tdeq_inv_pair1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H1 #L2 #HL12 destruct