proposition: Lemma allrel_cons2 x y xs ys : allrel (x :: xs) (y :: ys) = [&& r x y, all (r x) ys, all (r^~ y) xs & allrel xs ys].
proof: Proof. by rewrite /= allrel_consr -andbA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)