proposition: Lemma i_a_update_rec : forall m g s i e l, i_a m g (to_a1 e l) -> i_a m g (to_assert i (avar s)) -> i_a m g (to_a1 (ab_update e s i) l).
proof: Proof. intros m' g s i; induction e; simpl; intros l He Hi; auto. destruct a as (s1, i1'); destruct (string_dec s s1); simpl. destruct (to_syn i); destruct (to_syn i1'); subst s1; destruct (str_in_list s l); simpl in He |- *; intuition auto. destruct (to_syn i1'); destruct (str_in_list s1 l); simpl in He |- *; intuition auto. Qed.
imports: syntax little denot Bool List String ZArith axiom