proposition: Lemma injective_compose_with : forall u v w : E, strong_axioms u -> strong_axioms v -> injective w -> composable w u -> composable w v -> compose w u = compose w v -> u = v.
proof: Proof. ir. ap extens; au. transitivity (source (compose w u)). rewrite source_compose; au. rewrite H4. rewrite source_compose; au. unfold composable in H2, H3. xe. transitivity (source w); au. ir. unfold injective in H1. xe. unfold Transformation.injective in H7. xe. ap H8. unfold strong_axioms in H. xe. unfold axioms in H. unfold property in H. unfold composable in H2. xe. rewrite H11. ap H. am. unfold composable in H3; xe. rewrite H10. unfold strong_axioms in v; xe. au. transitivity (ev (compose w u) x). rewrite ev_compose; au. rewrite H4. rewrite ev_compose; au. Qed.
imports: Arith functions