More consistent names for `fill` lemmas of `LanguageCtx`.

I now consistently use _inv for the reverse direction, as we already used to do at various places. For example:

Lemma reducible_fill `{!@LanguageCtx Λ K} e σ :
  reducible e σ → reducible (K e) σ.
Lemma reducible_fill_inv `{!@LanguageCtx Λ K} e σ :
  to_val e = None → reducible (K e) σ → reducible e σ.