proposition: Lemma i_a_update : forall m g s i e, i_a m g (to_a e) -> i_a m g (to_assert i (avar s)) -> i_a m g (to_a (ab_update e s i)).
proof: Proof. intros m' g s i e; exact (i_a_update_rec m' g s i e nil). Qed.
imports: syntax little denot Bool List String ZArith axiom