proposition: Lemma setP_i y x : sub y x -> inc y (\Po x).
proof: Proof. have fp: forall a:x, inc (Yo (inc (Ro a) y) C0 C1) C2. by move => a; Ytac h; fprops. move => sxy; apply/IM_P; exists (fun a => Bo (fp a)); set_extens t. by move => ty; apply:(Zo_i (sxy _ ty)) => hyp; rewrite B_eq B_eq; Ytac0. move /Zo_P => [tz h]; move: (h tz); rewrite B_eq. by Ytac w; [ move: w; rewrite B_eq | move: C1_ne_C0 ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)