proposition: Lemma eq_allrel_memr {T} {S : eqType} (r : T -> S -> bool) s1 (s2 s2' : seq S) : s2 =i s2' -> allrel r s1 s2 = allrel r s1 s2'.
proof: Proof. by rewrite ![allrel _ s1 _]allrelC; apply: eq_allrel_meml. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)