proposition: Theorem equalBeforeREval : forall (f g : rNat -> bool) (e : rExpr), equalBefore (rnext (maxVar e)) f g -> rEval f e = rEval g e.
proof: Proof. intros f g e H'. apply support; auto with stalmarck. intros n H'0. apply equalBeforeElim with (n := rnext (maxVar e)); auto with stalmarck. apply inLt; auto with stalmarck. Qed.
imports: Coq(Relation_Definitions)