proposition: Lemma allrel_sub_l (r : T -> S -> bool) (xs xs' : seq T) (ys : seq S) : {subset xs' <= xs} -> 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)