proposition: Lemma carre : forall a u, axioms a -> mor (osource a) u -> comp (otarget a) (ntrans a (target u)) (fmor (source a) u)= comp (otarget a) (fmor (target a) u) (ntrans a (source u)).
proof: Proof. ir. uh H; xd. Qed.
imports: Arith functor