---

Step * 1 of Lemma uncurry_wf

.....basecase..... 
1. T : Type
2. n : ℤ
⊢ ∀[A:ℕ0 ⟶ Type]. ∀[f:funtype(0;A;T)].  (uncurry(0;f) ∈ (i:ℕ0 ⟶ A[i]) ⟶ T)
BY
{ xxx(RepUR ``funtype uncurry`` 0 THEN Auto)xxx }

---

Latex:

---

Latex:
.....basecase..... 
1.  T  :  Type
2.  n  :  \mBbbZ{}
\mvdash{}  \mforall{}[A:\mBbbN{}0  {}\mrightarrow{}  Type].  \mforall{}[f:funtype(0;A;T)].    (uncurry(0;f)  \mmember{}  (i:\mBbbN{}0  {}\mrightarrow{}  A[i])  {}\mrightarrow{}  T)


By

---

Latex:
xxx(RepUR  ``funtype  uncurry``  0  THEN  Auto)xxx

---

Home Index