proposition: Lemma allrel_rev2 {T S : Type} (r : T -> S -> bool) (s1 : seq T) (s2 : seq S) : allrel r (rev s1) (rev s2) = allrel r s1 s2.
proof: Proof. by rewrite allrel_revr allrel_revl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)