proposition: Lemma hcompose_axioms : forall a b, axioms a -> axioms b -> osource a = otarget b -> axioms (hcompose a b).
proof: Proof. ir. uf hcompose. rw vcompose_axioms. tv. ap htrans_right_axioms. nw. am. rw H1. tv. ap htrans_left_axioms. nw. am. am. rw source_htrans_right. rw target_htrans_left. tv. Qed.
imports: Arith functor