proposition: Lemma like_arrow_like : forall u, like u -> Arrow.like u.
proof: Proof. ir. uh H. uhg. ufi create H. set (f:=Function.create (U (source u)) (ev u)) in H. assert (arrow u = f). wr H. rw Arrow.arrow_create. tv. rw H0. sy; am. Qed.
imports: Arith functions