proposition: Lemma af'_correct : forall r1 e v g, aeval r1 e v -> af' (r1@g) e = v.
proof: Proof. intros r1 e v g H; induction H; simpl; auto. case (string_dec x x); auto. intros Habs; elim Habs; auto. simpl in IHaeval; case (string_dec y x); auto. intros Hxy ; assert (Habs:x<>y) by auto; elim Habs; auto. rewrite IHaeval1; rewrite IHaeval2; auto. Qed.
imports: syntax little denot Bool List String ZArith