proposition: Lemma chainE (T : poset) (s1 s2 : chain T) : s1 = s2 <-> pred_of s1 =p pred_of s2.
proof: Proof. split=>[->//|]; move: s1 s2=>[s1 H1][s2 H2] /= E; move: H1 H2. suff: s1 = s2 by move=>-> H1 H2; congr Chain; apply: proof_irrelevance. by apply: fext=>x; apply: pext; split; move/E. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype) LemmaOverloading(rels prelude)