-lemma lift_inv_bind1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
- ∀I,V1,U1. T1 = 𝕓{I} V1.U1 →
- ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 &
- T2 = 𝕓{I} V2. U2.
+fact lift_inv_bind1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
+ ∀I,V1,U1. T1 = 𝕓{I} V1.U1 →
+ ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 &
+ T2 = 𝕓{I} V2. U2.