proposition: Lemma i_a_a_subst_to_a_ignored : forall m g x a e l, str_in_list x l = true -> i_a m g (to_a1 e l) -> i_a m g (a_subst (to_a1 e l) x a).
proof: Proof. intros m' g x a; induction e; intros l Heq; simpl; auto. rewrite subst_to_assert; simpl; auto. destruct a0; simpl; case_eq (str_in_list s l); simpl; auto. destruct (to_syn t0); intros Hs0nl [Hs0 Htl]; split. rewrite subst_to_assert. simpl subst. destruct (string_dec x s) as [Hss0 | Hsns0]; auto. rewrite Hss0 in Heq; rewrite Heq in Hs0nl; discriminate. apply IHe; simpl; destruct (string_dec x s); auto. Qed.
imports: syntax little denot Bool List String ZArith axiom