proposition: Lemma fmor_vee_functor_catyd_arrow :forall a u v (y:morsy vee_data), vee_hypothesis a u v -> fmor (vee_functor a u v) (catyd_arrow y) = match y with i1 => id a (source u) | i2 => id a (target u) | i3 => id a (source v) | a12 => u | a32 => v end.
proof: Proof. ir. cp (vee_fun_data_property H). uf vee_functor. nin y; rww fmor_funtyd_catyd_arrow. Qed.
imports: Arith cat_examples cardinal fc_limits