proposition: Lemma left_fidentity : forall a f, axioms f -> a = target f -> fcompose (fidentity a) f = f.
proof: Proof. ir. rw H0; clear H0. ap axioms_extensionality; ir. fw'. am. fw. fw. rwi source_fcompose H0. fw'. Qed.
imports: Arith category