proposition: Lemma ab_lookup_i_a_rec : forall e ig s g, ~str_in_list s ig=true -> i_a m g (to_a1 e ig) -> i_a m g (to_assert (ab_lookup e s) (avar s)).
proof: Proof. induction e; intros ig s g Hi; simpl. unfold ab_lookup; simpl; intros; unfold to_assert. generalize (to_syn_ok bot (g s)); simpl. destruct (to_syn bot) as [bs bl]; intros Hok; assert(Hok' := Hok bs bl). simpl; rewrite lf'_app; rewrite lf_lz_to_a; rewrite f_p_lookup; simpl. rewrite <- (Hok' (syntax.lookup string_dec m (fun _ => True) bs)); auto. apply bot_semantics. destruct a as [s' i']; destruct (string_dec s s') as [Hses' | Hsns']; simpl. subst s'; destruct (str_in_list s ig);try (elim Hi; auto; fail). destruct (to_syn i') as [ _ _ ]; unfold ab_lookup; simpl. destruct (string_dec s s); intuition; fail. unfold ab_lookup; simpl; destruct (string_dec s' s). elim Hsns'; auto; fail. case_eq (str_in_list s' ig); simpl; intros Hin Hyp. apply IHe with (ig:=ig) (s:=s);auto. apply IHe with (ig:=s'::ig)(s:=s). simpl; destruct (string_dec s s'); contradiction || assumption. destruct (to_syn i'); simpl in * |- *; intuition. Qed.
imports: syntax little denot Bool List String ZArith axiom