proposition: Lemma allrelT {T S : Type} (xs : seq T) (ys : seq S) : allrel (fun _ _ => true) xs ys = true.
proof: Proof. by elim: xs => //= ? ?; rewrite allrel_consl all_predT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)