The no-selection statement, conditional on the separated chains

noSelection_of_separated: from SeparatedChainsContract and the proved limit analysis (family_limit) to NoSelectionContract.

theorem AVenhance.Infra.FullTheorem.noSelection_of_separated (β C₀ : ℝ) (hS : SeparatedChainsContract β C₀) : NoSelectionContract β C₀