proposition: Lemma CoUA_unic1 : forall (u : CoUA) (a' : A) (f : F a' --> b) (g : a' --> CoUA_ob u), FMor F g o CoUA_mor u =_S f -> CoUA_diese u f =_S g.
proof: Proof. intros u a' f g H; apply Sym; apply CoUA_unic; exact H. Qed.
imports: UniversalArrow Dual_Functor