proposition: Theorem equalBeforeNext : forall (f g : rNat -> bool) (n : rNat), equalBefore n f g -> f n = g n -> equalBefore (rnext n) f g.
proof: Proof. intros f g n H' H'0; red in H'; red in |- *; auto with stalmarck. intros m H'1; case (rNextInv m n); auto with stalmarck. intros H'2; rewrite H'2; auto with stalmarck. Qed.
imports: Coq(Relation_Definitions)