---

Step * 1 1 1 1 of Lemma cnv-taba-property


1. A : Type
2. B : Type
⊢ ∀ys:B List. ((0 ≤ ||ys||) ⇒ (<[], ys> = <[], ys> ∈ ((A × B) List × (B List))))
BY
{ Auto }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
\mvdash{}  \mforall{}ys:B  List.  ((0  \mleq{}  ||ys||)  {}\mRightarrow{}  (<[],  ys>  =  <[],  ys>))


By

---

Latex:
Auto

---

Home Index