proposition: Lemma beval_true_interpret : forall r b g, beval r b true -> bf' (r@g) b.
proof: Proof. intros r b g H; inversion H; simpl. rewrite (af'_correct r e1 v1); try rewrite (af'_correct r e2 v2); auto. Qed.
imports: syntax little denot Bool List String ZArith