-lemma tpr_fwd_shift_bind_minus: ∀L1,L2. |L1| = |L2| → ∀I1,I2,V1,V2,T1,T2.
- L1 @@ -ⓑ{I1}V1.T1 ➡ L2 @@ -ⓑ{I2}V2.T2 →
- L1 𝟙 L2 ∧ I1 = I2.
-#L1 #L2 #HL12 #I1 #I2 #V1 #V2 #T1 #T2 #H
-elim (tpr_fwd_shift1 (L1.ⓑ{I1}V1) … H) -H #Y #X #HY #HX
-elim (ltop_inv_pair1 … HY) -HY #L #V #HL1 #H destruct
-elim (shift_inj (L2.ⓑ{I2}V2) … HX ?) -HX
-[ #H1 #_ destruct /2 width=1/
-| lapply (ltop_fwd_length … HL1) -HL1 normalize //
-]
-qed-.
-