proposition: Lemma update_af'_diff : forall x v r1 r2 g s, s_update r1 x v r2 -> x <> s -> af' (r2@g)(avar s) = af' (r1@g) (avar s).
proof: Proof. intros x v r1 r2 g s H; induction H; intros Hnxs. simpl; case (string_dec x s). intros Hxs; elim Hnxs; auto. auto. simpl; case (string_dec y s); auto. Qed.
imports: syntax little denot Bool List String ZArith