proposition: Lemma cut_inc : forall (x : E) (p : x -> Prop) (y : x), p y -> inc (R y) (cut p).
proof: Proof. ir. unfold cut in |- *. ap Z_inc. ap R_inc. ir. assert (B hyp = y). ap R_inj. ap B_eq. rewrite H0. am. Qed.
imports: tactics