proposition: Lemma zmap_pr1 f a b: zmap f a b -> union f = a \cup b.
proof: Proof. move=> [pa pb]; set_extens t. move /setU_P => [y ty yf]; move: (pa _ yf) => /zprod2_P. by move=> [yu _ _]; apply: yu. move => tu; move: (pb _ tu) => [z [[zf xz] _]]; union_tac. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)