proposition: Lemma plot_ext : forall f g u d l, (forall x, f x = g x) -> plot1 f u d l -> plot1 g u d l.
proof: Proof. intros f g u d l H K i x Hx. specialize (K i x Hx). now rewrite <- H. Qed.
imports: Coq(Reals List) Sig Generic_proof Interval_helper Xreal Interval Tree Reify Prog