proposition: Lemma UniqueI : forall (i : Initial) (b : C), At_most_1mor (Initial_ob i) b.
proof: Proof. intros i b; red in |- *; intros f g. apply Trans with (MorI i b). apply (Prf_isInitial (i:=i)). apply Sym; apply (Prf_isInitial (i:=i)). Qed.
imports: Dual