-
-lemma lhap_fwd_le: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → is_le s.
-#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 /3 width=3/
-#a1 #s #M1 #M #HM1 #IHM1
-generalize in match HM1; -HM1
-cases IHM1 -s -M -M2 //
-#a #M0 #M #HM0 #s #M2 #_ #HM10 #H -M2
-lapply (lhap1_fwd_le … HM10 … HM0) -M -M0 -M1 /2 width=1/
-qed-.