proposition: Lemma arrow_create : arrow create = L (U (source create)) (ev create).
proof: Proof. uf create. rw Arrow.arrow_create. rw Arrow.source_create. uf ev. ap Function.create_extensionality. tv. ir. rw Arrow.arrow_create. rw Function.create_V_rewrite. tv. am. Qed.
imports: Arith functions