proposition: Lemma constant_prop6 f: constantfp f -> f = empty_function_tg (target f) \/ exists2 a, inc a (target f) & f = constant_function (source f) (target f) a.
proof: Proof. move => [pa pb]. case: (emptyset_dichot (source f)) => h. by left; rewrite {1} (empty_source_graph2 pa h). right; have h':=(rep_i h); have h'' := (Vf_target pa h'). ex_tac; apply: function_exten; rewrite/constant_function;aww. by apply: constant_f. by move => i isf; rewrite LfV //; apply: pb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)