proposition: Lemma powerset_inc : forall x y : E, sub x y -> inc x (powerset y).
proof: Proof. ir. unfold powerset in |- *. ap IM_inc. apply ex_intro with (fun b : y => inc (R b) x). ap extensionality. unfold sub in |- *. ir. pose (B H0). pose (B_eq H0). pose (cut_pr c). assert (x0 = R (cut_to c)). transitivity (R c). unfold c in |- *. au. sy. ap cut_to_R_eq. rewrite H1. am. unfold sub in |- *. ir. pose (B H0). pose (B_eq H0). rewrite <- e. unfold cut in |- *. ap Z_inc. ap H. rewrite e. am. ir. pose (B_eq hyp). rewrite e0. rewrite e. am. Qed.
imports: tactics