proposition: Lemma create_realizes : forall (x y : E) (f : E1), realizes x y f (create x y f).
proof: Proof. ir. pose source_create. pose target_create. pose ev_create. unfold realizes in |- *; xe. ir. au. Qed.
imports: Arith functions