proposition: Lemma lookup_aeval : forall r x v, lookup r x = Some v -> aeval r (avar x) v.
proof: Proof. Proof with auto. induction r; intros x v. simpl; intros; discriminate. destruct a as [y n]; simpl; case (string_dec y x)... intros Heq Heq2; injection Heq2; intros; subst... Qed.
imports: ZArith List syntax Lia