proposition: Lemma allrelC {T S : Type} (r : T -> S -> bool) xs ys : allrel r xs ys = allrel (fun y => r^~ y) ys xs.
proof: Proof. by elim: xs => [|x xs ih]; [elim: ys | rewrite allrel_consr -ih]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)