Define `fill` in terms of a `foldl` over `fill_item`.

This has some advantages:

• Evaluation contexts behave like a proper "Huet's zipper", and thus:

  • We no longer need to reverse the list of evaluation context items in the reshape_expr tactic.
  • The fill function becomes tail-recursive.

• It gives rise to more definitional equalities in simulation proofs using binary logical relations proofs.

  In the case of binary logical relations, we simulate an expressions in some ambient context, i.e. fill K e. Now, whenever we reshape e by turning it into fill K' e', we end up with fill K (fill K' e'). In order to use the rules for the expression that is being simulated, we need to turn fill K (fill K' e') into fill K'' e' for some K'. In case of the old foldr-based approach, we had to rewrite using the lemma fill_app to achieve that. However, in case of the old foldl-based fill, we have that fill K (fill K' e') is definitionally equal to fill (K' ++ K) e' provided that K' consists of a bunch of conses (which is always the case, since we obtained K' by reshaping e).

Note that this change hardly affected heap_lang. Only the proof of atomic_correct broke. I fixed this by proving a more general lemma ectxi_language_atomic about ectxi-languages, which should have been there in the first place.