proposition: Lemma allrel_sub_r (r : T -> S -> bool) (xs : seq T) (ys ys' : seq S) : {subset ys' <= ys} -> allrel r xs ys -> allrel r xs ys'.
proof: Proof. move=>H Ha; apply/allrelP=>x y Hx Hy. by move/allrelP: Ha; apply=>//; apply: H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq eqtype path fintype finfun tuple interval perm fingroup) pcm(options prelude ordtype seqext slice)