proposition: Lemma id_chainE (M : monotone id) : [id ^^ s by M] = s.
proof: Proof. by apply/chainE=>x; split; [case=>y [<-]|exists x]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)