proposition: Lemma rat_inf_limit_eq : forall f a1 a2, rat_inf_limit f a1 -> a1 == a2 -> rat_inf_limit f a2.
proof: Proof. unfold rat_inf_limit, inf_limit in *. intuition. edestruct H; eauto. exists x. intuition. rewrite <- H0. eapply H2. eapply H3. trivial. Qed.
imports: Arith FCF.Fold List FCF.StdNat FCF.Rat Arith