-lemma tpr_inv_lref1: ∀i,U2. #i ⇒ U2 → U2 = #i.
-/2/ qed.
-
-lemma tpr_inv_abbr1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Abbr} V1. T1 →
- ∨∨ ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abbr} V2. T2
- | ∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
- ⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
- U2 = 𝕚{Abbr} V2. T
- | ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2.
-#U1 #U2 * -U1 U2
-[ #k #V #T #H destruct
-| #i #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/
-| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
-| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
-| #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #V0 #T0 #H destruct -V1 T1 /3 width=7/
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
-| #V #T #T1 #T2 #HT1 #HT12 #V0 #T0 #H destruct -V T /3/
-| #V #T1 #T2 #_ #V0 #T0 #H destruct
-]
-qed.
-
-lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕚{Abbr} V1. T1 ⇒ U2 →
- ∨∨ ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abbr} V2. T2
- | ∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
- ⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
- U2 = 𝕚{Abbr} V2. T
- | ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2.
-/2/ qed.
-
-lemma tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Abst} V1. T1 →
- ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abst} V2. T2.
-#U1 #U2 * -U1 U2
-[ #k #V #T #H destruct
-| #i #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /2 width=5/
-| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
-| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
-| #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
-| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
-| #V #T1 #T2 #_ #V0 #T0 #H destruct
-]
-qed.
-
-lemma tpr_inv_abst1: ∀V1,T1,U2. 𝕚{Abst} V1. T1 ⇒ U2 →
- ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abst} V2. T2.
+lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 →
+ (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
+ ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T &
+ U2 = 𝕓{I} V2. T
+ ) ∨
+ ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2 & I = Abbr.