proposition: Lemma boundedSearch2 : forall (P : naryRel 2) (b : nat), boundedSearch P b = b \/ P b (boundedSearch P b) = true.
proof: Proof. unfold boundedSearch in |- *; intros P b. assert (H: forall P : naryRel 1, boundedSearchHelp P b = b \/ P (boundedSearchHelp P b) = true). { clear P; intros; induction b as [| b Hrecb]. - cbn in |- *; auto. - cbn in |- *. assert (H: P b = true \/ P b = false) by (destruct (P b); auto). induction (eq_nat_dec (boundedSearchHelp P b) b). induction H as [H| H]; rewrite H; auto. induction Hrecb as [H0| H0]. + elim b0; auto. + auto. } apply H. Qed.
imports: Coq(Arith Peano_dec Compare_dec List Eqdep_dec Utf8) hydras(extEqualNat misc Compat815) Coq(Lia)