proposition: Lemma ImageEq A B (f1 f2 : A -> B) (X : Pred A) : f1 =1 f2 -> Image f1 X =p Image f2 X.
proof: Proof. by move=>H x; split; case=>a ->; exists a. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)