-lemma cpy_inv_lift1_eq: ∀G,L,U1,U2,d,e.
- ⦃G, L⦄ ⊢ U1 ▶×[d, e] U2 → ∀T1. ⇧[d, e] T1 ≡ U1 → U1 = U2.
-#G #L #U1 #U2 #d #e #H elim H -G -L -U1 -U2 -d -e
-[ //
-| #I #G #L #K #V #W #i #d #e #Hdi #Hide #_ #_ #T1 #H
- elim (lift_inv_lref2 … H) -H * #H
- [ lapply (le_to_lt_to_lt … Hdi … H) -Hdi -H #H
- elim (lt_refl_false … H)
- | lapply (lt_to_le_to_lt … Hide … H) -Hide -H #H
- elim (lt_refl_false … H)
- ]
-| #a #I #G #L #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
- elim (lift_inv_bind2 … HX) -HX #V #T #HV1 #HT1 #H destruct
- >IHV12 // >IHT12 //
-| #I #G #L #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
- elim (lift_inv_flat2 … HX) -HX #V #T #HV1 #HT1 #H destruct
- >IHV12 // >IHT12 //
+lemma cpy_inv_lift1_eq: ∀G,T1,U1,d,e. ⇧[d, e] T1 ≡ U1 →
+ ∀L,U2. ⦃G, L⦄ ⊢ U1 ▶×[d, e] U2 → U1 = U2.
+#G #T1 #U1 #d #e #H elim H -T1 -U1 -d -e
+[ #k #d #e #L #X #H >(cpy_inv_sort1 … H) -H //
+| #i #d #e #Hid #L #X #H elim (cpy_inv_lref1 … H) -H //
+ * #I #K #V #H elim (ylt_yle_false … H) -H /2 width=1 by ylt_inj/
+| #i #d #e #Hdi #L #X #H elim (cpy_inv_lref1 … H) -H //
+ * #I #K #V #_ #H elim (ylt_yle_false i d)
+ /2 width=2 by ylt_inv_monotonic_plus_dx, yle_inj/
+| #p #d #e #L #X #H >(cpy_inv_gref1 … H) -H //
+| #a #I #V1 #W1 #T1 #U1 #d #e #_ #_ #IHVW1 #IHTU1 #L #X #H elim (cpy_inv_bind1 … H) -H
+ #W2 #U2 #HW12 #HU12 #H destruct /3 width=2 by eq_f2/
+| #I #V1 #W1 #T1 #U1 #d #e #_ #_ #IHVW1 #IHTU1 #L #X #H elim (cpy_inv_flat1 … H) -H
+ #W2 #U2 #HW12 #HU12 #H destruct /3 width=2 by eq_f2/