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