proposition: Lemma Image_inj_eqmem A B (f : A -> B) (X1 X2 : Pred A) : injective f -> Image f X1 =p Image f X2 -> X1 =p X2.
proof: Proof. by move=>H E; split; apply: Image_inj_sub H _ _; rewrite E. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)