proposition: Lemma diag_app_range a: Imf (diagonal_application a) = diagonal a.
proof: Proof. rewrite (ImfE (diag_app_f a)) [graph _] corresp_g;set_extens t. by move/Lg_range_P => [b ba ->]; apply/diagonal_pi_P. move/diagonal_i_P => [pt ta pq]; apply/Lg_range_P; ex_tac. by rewrite {2} pq pt. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)