proposition: Lemma in11_in2 (T1 T2 : predArgType) (P : T1 -> T2 -> Prop) (A1 : {pred T1}) (A2 : {pred T2}) : {in A1, forall x, {in A2, forall y, P x y}} <-> {in A1 & A2, forall x y, P x y}.
proof: Proof. by firstorder. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)