fix `head_stuck`

(From a discussion on Mattermost.)

The definition of head_stuck (in program_logic/ectx_language.v) was not what one would have expected. It was in fact equivalent to stuck (from program_logic/language.v), which also made redundant the additional assumption that sub_redexes_are_values in lemmas head_stuck_stuck and wp_lift_head_stuck (in program_logic/ectx_lifting.v). As a consequence, the latter lemma was a mere duplicate of its non-ectx counterpart wp_lift_stuck.

This commit changes the definition of head_stuck to the weaker property that one would have expected, and fixes the proof of head_stuck_stuck. The proof of wp_lift_head_stuck needs not be patched because it only uses head_stuck through the former lemma, whose expression has not changed.

@jung suggests to instead keep the definition as is, replace the lemma head_stuck_stuck by a proof of the equivalence with stuck, remove the assumption sub_redexes_are_values from the lifting lemma, and write a new lemma

head_redexes_are_values e → to_val e = None → head_irreducible e σ → head_stuck e σ

that permits the decomposition into simpler properties.

@jung and @jjourdan advice to gather @swasey’s opinion, given that he is the one who introduced this, and that he is using it in a number of developments.