proposition: Lemma scale_unique : forall u v : E, is_scale u -> is_scale v -> source u = source v -> target u = target v -> u = v.
proof: Proof. intros. apply extens. unfold is_scale in H; ee. unfold mor_axioms in H; xe. unfold is_scale in H0; ee. unfold mor_axioms in H0; xe. am. am. intros. apply scale_same_ev; au. Qed.
imports: universe