proposition: Theorem limit_f_eq : forall f1 f2 a, inf_limit f1 a -> (forall n a', (f1 n a' <-> f2 n a')) -> inf_limit f2 a.
proof: Proof. unfold inf_limit; intuition. destruct (H epsilon). trivial. exists x. intuition. eapply H2. eapply H3. eapply H0. trivial. Qed.
imports: Arith FCF.Fold List FCF.StdNat FCF.Rat