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