proposition: Lemma cf_injective I E: nonempty I -> injection (constant_functor I E).
proof: Proof. rewrite /constant_functor;move=> [x xi]. apply: lf_injective. move=> t te; apply/gfunctions_P2. split; aww. by move=> y /Lg_range_P [b be ->]. by move=> u v ue ve /(congr1 (Vg ^~ x)); rewrite !LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)