proposition: Lemma zmap_example1 a b: a <> b -> let A := singleton a in let B := singleton b in zmap (singleton (doubleton a b)) A B.
proof: Proof. move=> nab A B; rewrite /A/B. move: (setU2_11 a b); set (u := doubleton a b) => aux. split. by move=> t /set1_P ->; apply /zprod2_P; rewrite aux /u;split => //; [exists a | exists b]; apply:set1_pr; try (apply /setI2_P;split;fprops); move => z /setI2_P [_] /set1_P. rewrite aux; move=> x xu; exists u; split => //; first split; fprops. by move => t [] /set1_P. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)