{m : Type u → Type u_1} →
  {α : Type u} →
    [inst : LE α] →
      ({g : Type} → (lo hi : α) → lo ≤ hi → [RandomGen g] → Plausible.RandGT g m { a // lo ≤ a ∧ a ≤ hi }) →
        Plausible.BoundedRandom m α