R-to-L conversion is only defined for addresses that are alive.
Strengthen induction lemma for reflexive transitive closure.
Add map_Forall3.
Clean up ars.v.
Fix bug in interpreter.
Lemmas on Forall3 and tweak list tactics.
Reflexive transitive closure of executable semantics.
More undef/initial/final state definitions to state.v.
More concise weakening lemmas.

We have defined notions of memory environment and memory injection extensions
to capture the premises of the weakening lemmas in a more concise way.
Completeness of the executable semantics.