-include "lambda-delta/substitution/ps_ps.ma".
-include "lambda-delta/reduction/tpr_main.ma".
-include "lambda-delta/reduction/tpr_ps.ma".
-
-lemma ps_inv_lift_eq: ∀L,U1,U2,d,e.
- L ⊢ U1 [d, e] ≫ U2 → ∀T1. ↑[d, e] T1 ≡ U1 → U1 = U2.
-#L #U1 #U2 #d #e #H elim H -H L U1 U2 d e
-[ //
-| //
-| #L #K #V #U1 #U2 #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)
- ]
-| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
- elim (lift_inv_bind2 … HX) -HX #V #T #HV1 #HT1 #H destruct -X
- >IHV12 // >IHT12 //
-| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
- elim (lift_inv_flat2 … HX) -HX #V #T #HV1 #HT1 #H destruct -X
- >IHV12 // >IHT12 //
-]
-qed.
+include "lambda-delta/substitution/pts_pts.ma".
+include "lambda-delta/reduction/tpr_lift.ma".
+include "lambda-delta/reduction/tpr_pts.ma".