proposition: Lemma eq_in_allrel {T S : Type} (P : {pred T}) (Q : {pred S}) r r' : {in P & Q, r =2 r'} -> forall xs ys, all P xs -> all Q ys -> allrel r xs ys = allrel r' xs ys.
proof: Proof. move=> rr' xs ys Pxs Qys. by apply/idP/idP; apply/sub_in_allrel/Qys/Pxs => ? ? ? ?; rewrite rr'. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)