proposition: Theorem negligible_eq : forall (f1 f2 : nat -> Rat), negligible f1 -> (forall n, f1 n == f2 n) -> negligible f2.
proof: Proof. intuition. unfold negligible in *. intuition. edestruct H. econstructor. intuition. eapply H1. eauto. rewrite H3. rewrite <- H0. intuition. Qed.
imports: FCF.StdNat FCF.Rat