proposition: Lemma realizes_like_eq : forall (x y : E) (f : E1) (a : E), like a -> realizes x y f a -> create x y f = a.
proof: Proof. ir. ufi like H. wr H. ap create_extens; ufi realizes H0; xd. ir; sy; ap H2; am. Qed.
imports: Arith functions