proposition: Corollary Varacca_Winskel_Lemma_5_6 (Y Z : neset L) : hull Y = hull Z -> |_| Y = |_| Z.
proof: Proof. move=> H; rewrite -[in LHS]biglub_hull -[in RHS]biglub_hull. by congr (|_| _); apply neset_ext. Qed.
imports: HB(structures) Reals mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets Rstruct reals) mathcomp(finmap) Reals_ext realType_ext classical_sets_ext ssrR fdist fsdist convex