proposition: Lemma forall2_imset (aT rT : finType) (f g : aT -> rT) (p : {pred aT}) (q : rel rT) : [forall x in [set f z | z in p], forall y in [set g z | z in p], q x y] = [forall x in p, forall y in p, q (f x) (g y)].
proof: Proof. by rewrite forall_imset; under eq_forallb => y do rewrite forall_imset. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)