proposition: Lemma ex5_Y_prop2 J k x: nonempty J -> ex5_upper_bd J k -> forall t, inc t (ex5_Y J k x) <-> (inc t (Vg (psE S) k) /\ ex5_inY J k x t).
proof: Proof. move => ha hb t; split. move => tI; split; [ by apply: (ex5_Y_prop1 hb tI) | move => i iJ]. by move:(setIf_hi tI iJ) => /(ex5_Xij_pr (Vg x i) (proj2 hb _ iJ)) []. move => [hc hd]; apply/(setIf_P _ ha) => i iJ. apply/(ex5_Xij_pr (Vg x i) (proj2 hb _ iJ)); split => //;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)