proposition: Lemma image_chainP : chain_axiom [Pred x2 : T2 | exists x1, x2 = f x1 /\ x1 \In s].
proof: Proof. case: s=>p [[d H1] H2]; split=>[|x y]; first by exists (f d); exists d. case=>x1 [->] H3 [y1][->] H4; rewrite -!toPredE /= in H3 H4. by case: (H2 x1 y1 H3 H4)=>L; [left | right]; apply: M L. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)