proposition: Lemma ex : forall (x : E) (f : E1) (a : E), inc a (create x f) -> ex (fun b : E => A (inc b x) (f b = a)).
proof: Proof. ir. pose (IM_exists H). nin e. apply ex_intro with (R x0). xd. unfold inc in |- *. apply ex_intro with x0. tv. Qed.
imports: tactics