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