proposition: Lemma hcompose1_axioms : forall a b, hcomposable a b -> axioms (hcompose1 a b).
proof: Proof. ir. uh H; ee. uf hcompose1. rw vcompose_axioms. tv. ap htrans_left_axioms. nw. am. nw. ap htrans_right_axioms. nw. am. nw. rw source_htrans_left. rw target_htrans_right. tv. Qed.
imports: Arith functor