proposition: Lemma UniqueT : forall (t : Terminal) (a : C), At_most_1mor a (Terminal_ob t).
proof: Proof. intros t a; red in |- *; intros f g. apply Trans with (MorT t a). apply (Prf_isTerminal (t:=t)). apply Sym; apply (Prf_isTerminal (t:=t)). Qed.
imports: Dual