proposition: Lemma compose_axioms : forall u v : E, composable u v -> mor_axioms (compose u v).
proof: Proof. intros. unfold composable in H; ee. unfold mor_axioms in H; ee. unfold mor_axioms in H0; ee. unfold mor_axioms in |- *; ee. rewrite source_compose; au. rewrite target_compose; au. apply compose_strong_axioms. unfold Umorphism.composable in |- *; ee. apply axioms_from_strong; am. apply axioms_from_strong; am. am. intros. rewrite target_compose. rewrite ev_compose. rewrite ev_compose. rewrite source_compose in H8. apply H4. rewrite H1. apply H7. am. unfold axioms in H0; ee. rewrite source_compose in H8. lu. rewrite source_compose in H8. unfold axioms in H0; ee. lu. Qed.
imports: universe