proposition: Theorem support : forall (f g : rNat -> bool) (e : rExpr), (forall n : rNat, inRExpr n e -> f n = g n) -> rEval f e = rEval g e.
proof: Proof. intros f g e. elim e; intros; simpl in |- *; auto with stalmarck; rewrite H; auto with stalmarck; rewrite H0; auto with stalmarck. Qed.