proposition: Lemma to_a1_to_a_lookup : forall e g s l, i_a Ab.m g (to_a1 e l) -> str_in_list s l = false -> i_a Ab.m g (to_assert (ab_lookup e s)(avar s)).
proof: Proof. induction e. simpl. intros; apply to_assert_bot. destruct a as [s1 v]. intros g s l; unfold to_assert, ab_lookup; simpl. intros Hia Hin; destruct (string_dec s s1) as [Hss1 | Hsns1]. subst s1; rewrite Hin in Hia; simpl in Hia. destruct (to_syn v); destruct Hia as [H H0]. destruct (string_dec s s); try (intuition;fail). destruct (str_in_list s1 l). destruct (string_dec s1 s); [case Hsns1; auto; fail |idtac]. unfold to_assert,ab_lookup in IHe. apply IHe with l; auto. unfold to_assert, ab_lookup in IHe. destruct (string_dec s1 s);[elim Hsns1; intuition; fail|idtac]. apply IHe with (s1::l); simpl in *. destruct (to_syn v); simpl in Hia; intuition. destruct (string_dec s s1);intuition. Qed.
imports: syntax little denot Bool List String ZArith axiom