proposition: Lemma normNotEval : forall (p : rExpr) (f : rNat -> bool), rEval f (normNot p) = negb (rEval f p).
proof: Proof. intros; case p; simpl in |- *; auto with stalmarck; intros; rewrite negb_elim; auto with stalmarck. Qed.