proposition: Lemma Eq_powpow a b c: functions (b \times c) a \Eq functions c (functions b a).
proof: Proof. move:(@fpfa_fb a b c) => bf. exists (first_partial_map a b c). by split => //; rewrite /first_partial_map; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)