proposition: Lemma create_like : forall a : E, like (create (U a) (leq a)).
proof: Proof. ir. uf like. assert (U (create (U a) (leq a)) = U a). ap underlying_create. rw H. assert (leq (create (U a) (leq a)) = leq a). ap arrow_extensionality; ir. ap arrow_extensionality; ir. ap iff_eq; ir. rwi leq_create_all H0; ee; am. ufi leq H0. ee. rw leq_create_all; ee. am. am. uf leq; ee; am. rw H0. tv. Qed.
imports: universe