---

Step * 1 of Lemma reduce_wf


1. A : Type
2. B : Type
3. f : A ⟶ B ⟶ B
4. k : B
5. as : A List
⊢ reduce(f;k;as) ∈ B
BY
{ ListInd 5
THEN Reduce 0
THEN Auto }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B
4.  k  :  B
5.  as  :  A  List
\mvdash{}  reduce(f;k;as)  \mmember{}  B


By

---

Latex:
ListInd  5
THEN  Reduce  0
THEN  Auto

---

Home Index