Proof step 2 from proof choice-aux (previous step)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  ok(a), ∀ b. ok(b) → rel(b, elemf(b)) ∧ ok(elemf(b)) ⊦ ∃ nf. nf(0) = a ∧ ok(nf(0)) ∧ (∀ m. m < 0 → ok(nf(m)) ∧ nf(m + 1) = elemf(nf(m)))

• Proof step 5:

  ∀ a, elemf. ok(a) ∧ (∀ b. ok(b) → rel(b, elemf(b)) ∧ ok(elemf(b))) → (∃ nf. nf(0) = a ∧ ok(nf(n0)) ∧ (∀ m. m < n0 → ok(nf(m)) ∧ nf(m + 1) = elemf(nf(m)))), ok(a), ∀ b. ok(b) → rel(b, elemf(b)) ∧ ok(elemf(b)) ⊦ ∃ nf. nf(0) = a ∧ ok(nf(n0 +1)) ∧ (∀ m. m < n0 +1 → ok(nf(m)) ∧ nf(m + 1) = elemf(nf(m)))

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;;