proposition: Lemma carre_verbose_rw : forall a c1 f u, axioms a -> mor (osource a) u -> c1 = otarget a -> f = source a -> comp c1 (ntrans a (target u)) (fmor f u)= comp (otarget a) (fmor (target a) u) (ntrans a (source u)).
proof: Proof. ir. rw H1; rw H2. ap carre; am. Qed.
imports: Arith functor