---

Step * 1 1 of Lemma taba-property


1. A : Type
2. B : Type
3. init : B
4. F : A ⟶ A ⟶ B ⟶ B
5. xs : A List
⊢ ∀ys:A List. ((0 ≤ ||ys||) ⇒ (<init, ys> = <init, ys> ∈ (B × (A List))))
BY
{ Auto }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  init  :  B
4.  F  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B
5.  xs  :  A  List
\mvdash{}  \mforall{}ys:A  List.  ((0  \mleq{}  ||ys||)  {}\mRightarrow{}  (<init,  ys>  =  <init,  ys>))


By

---

Latex:
Auto

---

Home Index