proposition: Lemma Eq_powx1 x: (functions C1 x) \Eq x.
proof: Proof. exists (Lf (fun z => Vf z C0) (functions C1 x) x). saw;apply: lf_bijective. - move => t /functionsP [ft st tt]; Wtac; rewrite st; apply: set1_1. - move => u v /functionsP [fu su tu]/functionsP [fv sv tv] eq. by apply: (function_exten fu fv); (try ue); rewrite su => t/set1_P ->. - move => y yx; exists (constant_function C1 x y). apply/functionsP; exact: (constant_prop C1 yx). rewrite constant_V//; apply: set1_1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)