proposition: Lemma Eq_indexed a b: a \Eq (a *s1 b).
proof: Proof. rewrite /indexed. apply: (@equipotent_aux (fun x=> J x b)); apply: lf_bijective. - by move=> x xa /=; aw; fprops. - by move=> u v _ _; apply: pr1_def. - move=> y /setX_P [py pya /set1_P <-]; ex_tac; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)