proposition: Lemma ffunP (f1 f2 : fT) : (forall x, f1 x = f2 x) <-> f1 = f2.
proof: Proof. suffices ffunK f g: (forall x, f x = g x) -> f = finfun g. by split=> [/ffunK|] -> //; apply/esym/ffunK. case: f => f Dg; rewrite unlock; congr FinfunOf. have{} Dg x (aTx : mem_seq (enum aT) x): g x = fun_of_fin_rec f aTx. by rewrite -Dg /= (bool_irrelevance (mem_enum _ _) aTx). elim: (enum aT) / f (enum_uniq aT) => //= x1 s y f IHf /andP[s'x1 Us] in Dg *. rewrite Dg ?eqxx //=; case: eqP => // /eq_axiomK-> /= _. rewrite {}IHf // => x s_x; rewrite Dg ?s_x ?orbT //. by case: eqP (memPn s'x1 x s_x) => // _ _ /(bool_irrelevance s_x) <-. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple)