proposition: Lemma EqPredType_trans' (r1 r2 r3 : pT) : EqPredType r1 r2 -> EqPredType r2 r3 -> EqPredType r1 r3.
proof: Proof. by move=>H1 H2 x; split; [move/H1; move/H2 | move/H2; move/H1]. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)