proposition: Lemma scale_same_ev : forall u v x : E, is_scale u -> is_scale v -> source u = source v -> target u = target v -> inc x (U (source u)) -> ev u x = ev v x.
proof: Proof. intros. apply leq_leq_eq with (target u). unfold is_scale in H; ee. unfold mor_axioms in H; xe. rewrite H2. apply scale_leq_ev; au. apply scale_leq_ev; au. rewrite <- H1; am. Qed.
imports: universe