proposition: Lemma allrel_maskl m xs ys : allrel xs ys -> allrel (mask m xs) ys.
proof: Proof. by elim: m xs => [|[] m IHm] [|x xs] //= /andP [xys /IHm->]; rewrite ?xys. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)