/2 width=3/ qed.
(* Basic_1: was by definition: pr0_refl *)
-lemma tpr_refl: ∀T. T ➡ T.
+lemma tpr_refl: reflexive … tpr.
#T elim T -T //
#I elim I -I /2 width=1/
qed.
| ∃∃V,T. T ➡ #i & T1 = ⓝV. T.
/2 width=3/ qed-.
+(* Basic forward lemmas *****************************************************)
+
+lemma tpr_fwd_shift1: ∀L1,T1,T. L1 @@ T1 ➡ T →
+ ∃∃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-.
+
+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-.
+
(* Basic_1: removed theorems 3:
pr0_subst0_back pr0_subst0_fwd pr0_subst0
Basic_1: removed local theorems: 1: pr0_delta_tau