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.