proposition: Lemma allrel_catr xs ys ys' : allrel xs (ys ++ ys') = allrel xs ys && allrel xs ys'.
proof: Proof. elim: ys => /= [|y ys ihys]; first by rewrite allrel0r. by rewrite !allrel_consr ihys andbA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)