-lemma lift_inv_con22: ∀d,e,T1,I,V2,U2. ↑[d,e] T1 ≡ ♭I V2. U2 →
- ∃V1,U1. ↑[d,e] V1 ≡ V2 ∧ ↑[d+1,e] U1 ≡ U2 ∧
- T1 = ♭I V1. U1.
-#d #e #T1 #I #V2 #U2 #H lapply (lift_inv_con22_aux … H) /2/
+lemma lift_inv_bind2: ∀d,e,T1,I,V2,U2. ↑[d,e] T1 ≡ 𝕓{I} V2. U2 →
+ ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 &
+ T1 = 𝕓{I} V1. U1.
+#d #e #T1 #I #V2 #U2 #H lapply (lift_inv_bind2_aux … H) /2/
+qed.
+
+lemma lift_inv_flat2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
+ ∀I,V2,U2. T2 = 𝕗{I} V2.U2 →
+ ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 &
+ T1 = 𝕗{I} V1.U1.
+#d #e #T1 #T2 #H elim H -H d e T1 T2
+[ #k #d #e #I #V2 #U2 #H destruct
+| #i #d #e #_ #I #V2 #U2 #H destruct
+| #i #d #e #_ #I #V2 #U2 #H destruct
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V2 #U2 #H destruct
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V2 #U2 #H destruct /2 width = 5/
+]
+qed.
+
+lemma lift_inv_flat2: ∀d,e,T1,I,V2,U2. ↑[d,e] T1 ≡ 𝕗{I} V2. U2 →
+ ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 &
+ T1 = 𝕗{I} V1. U1.
+#d #e #T1 #I #V2 #U2 #H lapply (lift_inv_flat2_aux … H) /2/