proposition: Lemma eq_forallb_in D P1 P2 : (forall x, D x -> P1 x = P2 x) -> [forall (x | D x), P1 x] = [forall (x | D x), P2 x].
proof: Proof. by move=> eqP12; apply: eq_forallb => i; case Di: (D i); rewrite // eqP12. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)