proposition: Lemma cut_pr : forall (x : E) (p : x -> Prop) (y : cut p), p (cut_to y).
proof: Proof. ir. unfold cut_to in |- *. unfold cut in y. set (k := fun y : E => forall hyp : inc y x, p (B hyp)) in *. pose (R_inc y). Ztac. Qed.
imports: tactics