proposition: Lemma boundedSearch4 : forall (P : naryRel 2) (b : nat), P b b = true -> P b (boundedSearch P b) = true.
proof: Proof. intros; destruct (boundedSearch2 P b); auto. now rewrite H0. Qed.
imports: hydras(primRec extEqualNat ssrnat_extracts) Coq(Min ArithRing Lia Compare_dec Arith Lia)