fact: Fixpoint boundedSearchHelp (P : naryRel 1) (b : nat) {struct b} : nat := match b with | O => 0 | S b' => let q := boundedSearchHelp P b' in match eq_nat_dec q b' with | left _ => match P b' with | true => b' | false => S b' end | right _ => q end end.
imports: Coq(Arith Peano_dec Compare_dec List Eqdep_dec Utf8) hydras(extEqualNat misc Compat815) Coq(Lia)