proposition: Lemma fob_fcompose : forall f g x, axioms f -> axioms g -> source f = target g -> ob (source g) x -> fob (fcompose f g) x = fob f (fob g x).
proof: Proof. ir. uf fcompose. uf compose. rw fob_create. tv. fw'. cw. fw. fw. am. Qed.
imports: Arith category