proposition: Lemma is_subcategory_same_comp : forall a b, is_subcategory a b -> (forall u v, mor a u -> mor a v -> source u = target v -> comp a u v = comp b u v).
proof: Proof. ir. uh H; ee. au. Qed.
imports: Arith ordinal nat_trans