Rename lemma `not_stuck_under_ectx` → `not_stuck_fill`, to be consistent with `stuck_fill`.
Also refactor the proofs to make better reuse of existing lemmas.
The lemma not_stuck_under_ectx
was created as part of !275 (merged) so is not used anywhere yet but in the prophecy erasure proof.