proposition: Lemma zequiv_empty M: ziequivalent M emptyset -> M = emptyset.
proof: Proof. move=> [_ [f zm]]; apply /set0_P => x xM. have xu: (inc x (M \cup emptyset)) by rewrite setU2_0. by move: (in_set0 (zmap_val_pr1b zm xu)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)