---

Step * 1 of Lemma tuple-sum-wf-partial


1. P : Type
2. G : P ⟶ Type
3. f : i:P ⟶ (G i) ⟶ partial(ℕ)
4. u : P
5. v : P List
6. ∀[x:tuple-type(map(G;v))]. (tuple-sum(f;v;x) ∈ partial(ℕ))
7. null(v) = tt
⊢ ∀[x@0:G u]. (f u x@0 ∈ partial(ℕ))
BY
{ Auto }

---

Latex:

---

Latex:

1.  P  :  Type
2.  G  :  P  {}\mrightarrow{}  Type
3.  f  :  i:P  {}\mrightarrow{}  (G  i)  {}\mrightarrow{}  partial(\mBbbN{})
4.  u  :  P
5.  v  :  P  List
6.  \mforall{}[x:tuple-type(map(G;v))].  (tuple-sum(f;v;x)  \mmember{}  partial(\mBbbN{}))
7.  null(v)  =  tt
\mvdash{}  \mforall{}[x@0:G  u].  (f  u  x@0  \mmember{}  partial(\mBbbN{}))


By

---

Latex:
Auto

---

Home Index