proposition: Lemma create_like : forall (x y : E) (f : E1), like (create x y f).
proof: Proof. ir. uf like. ap create_extens. ap source_create. ap target_create. ir. ap ev_create. rwi source_create H. am. Qed.
imports: Arith functions