proposition: Lemma eq_allrel_mem2 {T S : eqType} (r : T -> S -> bool) (s1 s1' : seq T) (s2 s2' : seq S) : s1 =i s1' -> s2 =i s2' -> allrel r s1 s2 = allrel r s1' s2'.
proof: Proof. by move=> /eq_allrel_meml -> /eq_allrel_memr ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)