proposition: Lemma subst_fpw : forall g s e' e, af' g (subst e s e') = af' (fpw g s (af' g e')) e.
proof: Proof. intros g x e' e; induction e; simpl; auto. unfold fpw; destruct (string_dec x s); auto. rewrite IHe1; rewrite IHe2; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom