proposition: Lemma allrel_trans (xs ys : seq S) z r : transitive r -> all (r^~ z) xs -> all (r z) ys -> allrel r xs ys.
proof: Proof. move=>Ht /allP Ha /allP Hp; apply/allrelP=>x y + Hy. by move/Ha/Ht; apply; apply: Hp. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq eqtype path fintype finfun tuple interval perm fingroup) pcm(options prelude ordtype seqext slice)