proposition: Lemma left_id_unique : forall a e x, axioms a -> mor a e -> source e = x -> (forall f, composable a e f -> comp a e f = f) -> e = id a x.
proof: Proof. ir. rwi mor_facts_rw H0. wr H1. uh H0; ee. transitivity (comp a e (id a x)). rw right_id; try tv; try lu. wr H1; am. wr H2. wr H1; tv. ap show_composable. am. rwi ob_facts_rw H3; uh H3; ee; am. rwi ob_facts_rw H3; uh H3; ee; sy; am. Qed.
imports: Arith universe