proposition: Lemma ab_lookup_i_a : forall e s g, i_a Ab.m g (to_a e) -> i_a Ab.m g (to_assert (ab_lookup e s) (avar s)).
proof: Proof. unfold to_a; intros e s g; apply (ab_lookup_i_a_rec e nil s g); simpl; discriminate. Qed.
imports: syntax little denot Bool List String ZArith axiom