+
+lemma lsred_lift: ∀p. liftable (lsred p).
+#p #h #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/
+#B #A #d <dsubst_lift_le //
+qed.
+
+lemma lsred_inv_lift: ∀p. deliftable_sn (lsred p).
+#p #h #N1 #N2 #H elim H -p -N1 -N2
+[ #D #C #d #M1 #H
+ elim (lift_inv_appl … H) -H #B #M #H0 #HM #H destruct
+ elim (lift_inv_abst … HM) -HM #A #H0 #H destruct /3 width=3/
+| #p #C1 #C2 #_ #IHC12 #d #M1 #H
+ elim (lift_inv_abst … H) -H #A1 #HAC1 #H
+ elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
+ @(ex2_intro … (𝛌.A2)) // /2 width=1/
+| #p #D1 #D2 #C1 #_ #IHD12 #d #M1 #H
+ elim (lift_inv_appl … H) -H #B1 #A #HBD1 #H1 #H2
+ elim (IHD12 … HBD1) -D1 #B2 #HB12 #HBD2 destruct
+ @(ex2_intro … (@B2.A)) // /2 width=1/
+| #p #D1 #C1 #C2 #_ #IHC12 #d #M1 #H
+ elim (lift_inv_appl … H) -H #B #A1 #H1 #HAC1 #H2
+ elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
+ @(ex2_intro … (@B.A2)) // /2 width=1/
+]
+qed-.
+
+lemma lsred_dsubst: ∀p. dsubstable_dx (lsred p).
+#p #D1 #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/
+#D2 #A #d >dsubst_dsubst_ge //
+qed.
+
+theorem lsred_mono: ∀p. singlevalued … (lsred p).
+#p #M #N1 #H elim H -p -M -N1
+[ #B #A #N2 #H elim (lsred_inv_nil … H ?) -H // #D #C #H #HN2 destruct //
+| #p #A1 #A2 #_ #IHA12 #N2 #H elim (lsred_inv_sn … H ??) -H [4: // |2: skip ] * (**) (* simplify line *)
+ [ #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/
+ | #D1 #D2 #C #_ #H destruct
+ ]
+| #p #B1 #B2 #A #_ #IHB12 #N2 #H elim (lsred_inv_sn … H ??) -H [4: // |2: skip ] * (**) (* simplify line *)
+ [ #C1 #C2 #_ #H destruct
+ | #D1 #D2 #C #HD12 #H #HN2 destruct /3 width=1/
+ ]
+| #p #B #A1 #A2 #_ #IHA12 #N2 #H elim (lsred_inv_dx … H ??) -H [3: // |2: skip ] #D #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/ (**) (* simplify line *)
+]
+qed-.