proposition: Lemma equalBeforerZEval : forall (f g : rNat -> bool) (n : rNat) (p : rZ), rVlt p n -> equalBefore n f g -> rZEval f p = rZEval g p.
proof: Proof. intros f g n p; case p; unfold rVlt in |- *; simpl in |- *; auto with stalmarck. intros r H' H'0; red in H'0; auto with stalmarck. rewrite (H'0 r); auto with stalmarck. Qed.
imports: Coq(Relation_Definitions)