proposition: Lemma vident_hcomposable : forall f g, Functor.axioms f -> Functor.axioms g -> source f = target g -> hcomposable (vident f) (vident g).
proof: Proof. ir. uhg; ee. rww vident_axioms. rww vident_axioms. rw osource_vident. rww otarget_vident. Qed.
imports: Arith functor