proposition: Lemma ImageU A B (f : A -> B) (X1 X2 : Pred A) : Image f (PredU X1 X2) =p [PredU Image f X1 & Image f X2].
proof: Proof. move=>x; split. - by case=>y -> [H|H]; [left | right]; apply: Image_mem. by case; case=>y -> H; apply: Image_mem; [left | right]. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)