proposition: Lemma Exercise4_8p f: function f -> target f = E48I -> char_fun (Vfi1 f \1c) (source f) = f.
proof: Proof. move=> ff tf;rewrite /char_fun; apply: function_exten; aw; trivial. apply: char_fun_f. by rewrite tf. move=> x xs; rewrite /Vfi1 LfV//; last by apply: char_fun_axioms. move: (Vf_target ff xs); rewrite tf; case /set2_P => wf. rewrite /varianti Y_false //; move /iim_graph_P => [u] /set1_P -> h. move: (Vf_pr ff h); rewrite wf; fprops. rewrite /varianti Y_true //; apply /iim_graph_P; exists \1c; fprops. by rewrite -wf; apply: Vf_pr3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)