---

Step * of Lemma dependent-choice

∀[T:ℕ ⟶ Type]. ∀[R:n:ℕ ⟶ T[n] ⟶ T[n + 1] ⟶ ℙ].
  ((∀n:ℕ. ∀x:T[n].  ∃y:T[n + 1]. R[n;x;y])
  ⇒ (∀x0:T[0]. ∃f:n:ℕ ⟶ T[n]. (((f 0) = x0 ∈ T[0]) ∧ (∀n:ℕ. R[n;f n;f (n + 1)]))))
BY
{ (Auto THEN (Skolemize  (-2) `F' THENA Auto)) }

1
1. [T] : ℕ ⟶ Type
2. [R] : n:ℕ ⟶ T[n] ⟶ T[n + 1] ⟶ ℙ
3. ∀n:ℕ. ∀x:T[n].  ∃y:T[n + 1]. R[n;x;y]
4. x0 : T[0]
5. F : n:ℕ ⟶ x:T[n] ⟶ T[n + 1]
6. ∀n:ℕ. ∀x:T[n].  R[n;x;F n x]
⊢ ∃f:n:ℕ ⟶ T[n]. (((f 0) = x0 ∈ T[0]) ∧ (∀n:ℕ. R[n;f n;f (n + 1)]))

---

Latex:

---

Latex:
\mforall{}[T:\mBbbN{}  {}\mrightarrow{}  Type].  \mforall{}[R:n:\mBbbN{}  {}\mrightarrow{}  T[n]  {}\mrightarrow{}  T[n  +  1]  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}n:\mBbbN{}.  \mforall{}x:T[n].    \mexists{}y:T[n  +  1].  R[n;x;y])
    {}\mRightarrow{}  (\mforall{}x0:T[0].  \mexists{}f:n:\mBbbN{}  {}\mrightarrow{}  T[n].  (((f  0)  =  x0)  \mwedge{}  (\mforall{}n:\mBbbN{}.  R[n;f  n;f  (n  +  1)]))))


By

---

Latex:
(Auto  THEN  (Skolemize    (-2)  `F'  THENA  Auto))

---

Home Index