---

Step * of Lemma uncurry_wf

∀[T:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[f:funtype(n;A;T)].  (uncurry(n;f) ∈ (i:ℕn ⟶ A[i]) ⟶ T)
BY
{ xxxInductionOnNatxxx }

1
.....basecase..... 
1. T : Type
2. n : ℤ
⊢ ∀[A:ℕ0 ⟶ Type]. ∀[f:funtype(0;A;T)].  (uncurry(0;f) ∈ (i:ℕ0 ⟶ A[i]) ⟶ T)

2
.....upcase..... 
1. T : Type
2. n : ℤ
3. 0 < n
4. ∀[A:ℕn - 1 ⟶ Type]. ∀[f:funtype(n - 1;A;T)].  (uncurry(n - 1;f) ∈ (i:ℕn - 1 ⟶ A[i]) ⟶ T)
⊢ ∀[A:ℕn ⟶ Type]. ∀[f:funtype(n;A;T)].  (uncurry(n;f) ∈ (i:ℕn ⟶ A[i]) ⟶ T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[A:\mBbbN{}n  {}\mrightarrow{}  Type].  \mforall{}[f:funtype(n;A;T)].    (uncurry(n;f)  \mmember{}  (i:\mBbbN{}n  {}\mrightarrow{}  A[i])  {}\mrightarrow{}  T)


By

---

Latex:
xxxInductionOnNatxxx

---

Home Index