proposition: Lemma Z_inc : forall (x : E) (p : EP) (y : E), inc y x -> p y -> inc y (Z x p).
proof: Proof. ir. unfold Z in |- *. eapply IM_inc. unfold inc in H. nin H. assert (p (R x0)). rewrite H. am. pose (join (f:=fun a : x => p (R a)) x0 H1). apply ex_intro with r. tv. Qed.
imports: tactics