proposition: Lemma i_a_ab_update_rec : forall m a g i e x l, i_a m g (to_a1 e l) -> i_a m g (to_assert i a) -> i_a m g (a_subst (to_a1 (ab_update e x i) l) x a).
proof: Proof. intros m' a g i e x; induction e; intros l Hyp Ha; simpl; auto. rewrite subst_to_assert; simpl; auto. destruct a0. destruct (string_dec x s); simpl. case_eq (str_in_list s l); intros Hin. apply i_a_a_subst_to_a_ignored. subst s; auto. simpl in Hyp; rewrite Hin in Hyp; intuition; fail. destruct (to_syn i); simpl; split. rewrite subst_to_assert; simpl; destruct (string_dec x s); intuition ; fail. apply i_a_a_subst_to_a_ignored. simpl; destruct (string_dec x s); try contradiction; auto. simpl in Hyp; destruct (to_syn t0); rewrite Hin in Hyp; simpl in Hyp; intuition;fail. case_eq (str_in_list s l); intros Hin. apply IHe; simpl in Hyp; rewrite Hin in Hyp; intuition;fail. destruct (to_syn t0); simpl; split. rewrite subst_to_assert; unfold l_subst, subst. destruct (string_dec x s);try contradiction. simpl in Hyp; destruct (to_syn t0); rewrite Hin in Hyp; simpl in Hyp; intuition;fail. apply IHe; auto. simpl in Hyp; destruct (to_syn t0); rewrite Hin in Hyp; simpl in Hyp; intuition. Qed.
imports: syntax little denot Bool List String ZArith axiom