- ∃∃L2,T2. L1 𝟙 L2 & T = L2 @@ T2.
-#L1 @(lenv_ind_dx … L1) -L1
-[ #T1 #T #_ @ex2_2_intro [3: // |4: // |1,2: skip ] (**) (* /2 width=4/ does not work *)
-| #I #L1 #V1 #IH #T1 #T >shift_append_assoc #H
- elim (tpr_inv_bind1 … H) -H *
- [ #V0 #T0 #X0 #_ #HT10 #HTX0 #H destruct
- elim (IH … HT10) -IH -T1 #L2 #V2 #HL12 #H destruct
- elim (tps_fwd_shift1 … HTX0) -V2 #L3 #X3 #HL23 #H destruct
- lapply (ltop_trans … HL12 HL23) -L2 #HL13
- @(ex2_2_intro … (⋆.ⓑ{I}V0@@L3)) /2 width=4/ /3 width=1/
- | #T0 #_ #_ #H destruct
- ]
-]
-qed-.
-*)
-
-
-(*
- >shift_append_assoc >shift_append_assoc >shift_append_assoc >shift_append_assoc normalize #H
+ ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
+#L1 @(lenv_ind_dx … L1) -L1 normalize
+[ #T1 #T #HT1
+ @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *)
+| #I #L1 #V1 #IH #T1 #X
+ >shift_append_assoc normalize #H