proposition: Lemma In_map_snd_const : forall A (v : list A) f (a b : Q), In a (map f v) -> In (a,b) (map (fun x => (f x, b)) v).
proof: Proof. induction v. - intros. contradiction H. - intros. simpl. destruct H. subst a0. left. reflexivity. right. apply IHv, H. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.raster.Raster CoRN.reals.fast.Interval CoRN.metric2.FinEnum CoRN.metric2.ProductMetric CoRN.logic.Classic