proposition: Lemma sub_in_allrel {T S : Type} (P : {pred T}) (Q : {pred S}) (r r' : T -> S -> bool) : {in P & Q, forall x y, r x y -> r' x y} -> forall xs ys, all P xs -> all Q ys -> allrel r xs ys -> allrel r' xs ys.
proof: Proof. move=> rr' + ys; elim=> //= x xs IHxs /andP [Px Pxs] Qys. rewrite !allrel_consl => /andP [+ {}/IHxs-> //]; rewrite andbT. by elim: ys Qys => //= y ys IHys /andP [Qy Qys] /andP [/rr'-> // /IHys->]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)