proposition: Lemma Com_UAlaw2 : UA_law2 (Mor_com_ob axu_ob) Com_diese.
proof: Proof. unfold UA_law2, UA_eq in |- *; intros a' f g H. cut (Com_law (bxg:=Build_Com_ob f) g). intro H'. apply (UniqueI (Build_Com_arrow H') (MorI axu (Build_Com_ob f))); auto. unfold Com_law in |- *; simpl in |- *. apply Sym; trivial. Qed.
imports: Comma UniversalArrow