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