proposition: Lemma zmap_val_pr3a f a b x: zmap f a b -> inc x a -> (zmap_val f a (zmap_val f b x)) = x.
proof: Proof. move=> zm xa. have xu: inc x (union2 a b) by apply: setU2_1. move: (zmap_aux_pr1 zm xu) => [zf xz]. move: (zm) => [pa pb]; move: (pa _ zf) => xx. move: (zprod2_pr1 xx) => [pc pd]. set (t := zmap_val f b x); set y := zmap_aux f x. have: inc t (y \cap b) by rewrite pd; fprops. move /setI2_P => [ta1 ta2]. have tab: (inc t (a \cup b)) by apply: setU2_2. suff: y = zmap_aux f t. rewrite /zmap_val; move => <-;symmetry; apply: (zprod2_pr1a (pa _ zf) xa xz). apply: (zmap_aux_pr2 zm tab zf ta1). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)