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