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