proposition: Lemma const_chainE s : [_ ^^ s by const_mono] = const_chain.
proof: Proof. apply/chainE=>z1; split; first by case=>z2 [->]. by case: s=>s [[d] H1] H2 <-; exists d. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)