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