-fact tps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 →
+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 →