proposition: Lemma Eq_pow_inv A B C D: A \Eq B -> C \Eq D -> functions C A \Eq functions D B.
proof: Proof. move=> [f [bf sf tf]] /EqS [g [bg sg tg]]. exists (compose3function g f); hnf. rewrite {2 3} /compose3function - sf -tf - sg -tg; aw. by split => //;apply: c3f_fb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)