proposition: Lemma aeval_lookup : forall r e n, aeval r e n -> forall name, e = avar name -> lookup r name = Some n.
proof: Proof. intros r e n H; elim H; simpl. intros; discriminate. intros r0 x v name Heq; injection Heq; intros; subst. destruct (string_dec name name); intuition auto. intros r0 x y v v' Hneq Hev Hrec name Heq; injection Heq; intros; subst. destruct (string_dec y name); auto. intros; elim Hneq; auto. intros; discriminate. Qed.
imports: ZArith List syntax Lia