fact: Definition search_infinite_go (xs : list B) (n : nat) (go : ∀ n', R xs n' n → B) : B := let x := f n in match decide (x ∈ xs) with | left Hx => go (S n) (search_infinite_step xs n Hx) | right _ => x end.
imports: stdpp(relations pretty) stdpp(options)