-lemma lhap_lsreds_fwd: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → M1 ⇀*[s] M2.
-#s #M1 #M2 #H elim H -s -M1 -M2 //
-#p #M1 #M #HM1 #s #M2 #_ #IHM2
-lapply (lhap1_lsred_fwd … HM1) -HM1 /2 width=3/
+lemma head_lsreds_lhap: ∀s,M1,M2. M1 ⇀*[s] M2 → is_head s → M1 ⓗ⇀*[s] M2.
+#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
+#a #s #M1 #M #HM1 #_ #IHM2 * /3 width=3/
+qed.
+
+lemma lhap_inv_head: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → is_head s.
+#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
+#p #s #M1 #M #HM1 #_ #IHM2
+lapply (lhap1_inv_head … HM1) -HM1 /2 width=1/