proposition: Lemma mor_fc_extensionality : forall u v, (exists z, ( mor (function_cat z) u & mor (function_cat z) v & source u = source v & target u = target v & (forall x, inc x (source u) -> V x (arrow u) = V x (arrow v))))-> u = v.
proof: Proof. ir. nin H. ee. rwi mor_function_cat3 H. rwi mor_function_cat3 H0; ee. ap fa_extensionality. am. am. am. am. am. Qed.
imports: Arith ordinal nat_trans