proposition: Theorem normEval : forall (f : rNat -> bool) (e : Expr), Eval f e = rEval f (norm e).
proof: Proof. simple induction e; clear e; simpl in |- *; auto with stalmarck. intros p H; rewrite normNotEval; rewrite H; auto with stalmarck. intros b p Hp q Hq; case b; rewrite Hp; rewrite Hq; auto with stalmarck; rewrite normOrEval || rewrite normImplEval; auto with stalmarck. Qed.