proposition: Lemma otarget_twoarrow_nt : forall a u1 v1 u2 v2 r s, otarget (twoarrow_nt a u1 v1 u2 v2 r s) = a.
proof: Proof. ir. uf otarget. rw target_twoarrow_nt. rww target_twoarrow_functor. Qed.
imports: Arith cat_examples cardinal fc_limits