proposition: Corollary compose_identity_left E: {when (fun x => correspondence x /\ (target x) = E), left_id (identity E) compose}.
proof: Proof. move => x [cx <-]; exact:compf_id_left. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)