Work on using filter_dom in lift_memory.

I've made this change as an effort to fix some of the issues we're
running into with out of bounds addresses in the finite memory.

This has involved introducing and proving some lemmas about filter_dom
and in_bounds, culminating in a proof of
lift_memory_convert_memory_inversion, which seems like a good test
case for this change.

Note, the proof of lift_memory_convert_memory_inversion does depend on
a new admitted lemma:

  Lemma IntMaps_filter_dom_list_filter_Equal :
    forall {A : Type} (f : IntMaps.IM.key -> bool) (l : list (IntMaps.IM.key * A)),
      IntMaps.IM.Equal (IntMaps.IP.filter_dom f (IntMaps.IP.of_list l))
        (IntMaps.IP.of_list (filter (fun '(i, x) => f i) l)).
  Proof.
  Admitted.

However, this is similar to a previously admitted lemma anyway:

  Lemma IntMaps_map_list_map_Equal :
    forall {A B} (f : A -> B) l,
      IntMaps.IM.Equal (IntMaps.IM.map f (IntMaps.IP.of_list l)) (IntMaps.IP.of_list (List.map (fun '(i, x) => (i, f x)) l)).
  Proof.
  Admitted.