proposition: Lemma Z_pr : forall (x : E) (p : EP) (y : E), inc y (Z x p) -> p y.
proof: Proof. ir. unfold inc in H. nin H. unfold Z in x0. pose (R_inc x0). pose (IM_exists i). nin e. pose (tail x1). simpl in p0. rewrite H0 in p0. rewrite <- H. am. Qed.
imports: tactics