-#p #M1 #M2 #H
-elim (lsreds_inv_cons … H ???) -H [4: // |2,3: skip ] #M #HM1 #H (**) (* simplify line *)
-<(lsreds_inv_nil … H ?) -H //
-qed-.
-
-(* Note: "|s|" should be unparetesized *)
-lemma lsreds_fwd_mult: ∀s,M1,M2. M1 ⇀*[s] M2 → #{M2} ≤ #{M1} ^ (2 ^ (|s|)).
-#s #M1 #M2 #H elim H -s -M1 -M2 normalize //
-#p #M1 #M #HM1 #s #M2 #_ #IHM2
-lapply (lsred_fwd_mult … HM1) -p #HM1
-@(transitive_le … IHM2) -M2
-/3 width=1 by le_exp1, lt_O_exp, lt_to_le/ (**) (* auto: slow without trace *)