exists x+1
case succ.inl
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : p (x + 1) = true
⊢ ∃ y, y ≤ x + 1 ∧ p y = true
case succ.inl
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : p (x + 1) = true
⊢ x + 1 ≤ x + 1 ∧ p (x + 1) = true