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