proposition: Lemma eq_forall_in (T : finType) (A P1 P2 : {pred T}) : {in A, P1 =1 P2} -> [forall x in A, P1 x] = [forall x in A, P2 x].
proof: Proof. move=> eqP. apply/eq_forallb => x; case xA: (x \in A) => //=. exact: eqP. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)