-fact tps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 →
- ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
- ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 &
- L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ≫ T2 &
- U2 = 𝕓{I} V2. T2.
+lemma tps_inv_gref1: ∀L,T2,p,d,e. L ⊢ §p [d, e] ▶ T2 → T2 = §p.
+#L #T2 #p #d #e #H
+elim (tps_inv_atom1 … H) -H //
+* #K #V #i #_ #_ #_ #_ #H destruct
+qed-.
+
+fact tps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ▶ U2 →
+ ∀I,V1,T1. U1 = ⓑ{I} V1. T1 →
+ ∃∃V2,T2. L ⊢ V1 [d, e] ▶ V2 &
+ L. ⓑ{I} V2 ⊢ T1 [d + 1, e] ▶ T2 &
+ U2 = ⓑ{I} V2. T2.