---

Step * of Lemma testrec1_wf

No Annotations
∀[A:Type]. ∀[x:ℤ]. ∀[L:A List].  (testrec1(x;L) ∈ ℤ)
BY
{ ProveRecWfLemma `testrec1` `L'⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A:Type].  \mforall{}[x:\mBbbZ{}].  \mforall{}[L:A  List].    (testrec1(x;L)  \mmember{}  \mBbbZ{})


By

---

Latex:
ProveRecWfLemma  `testrec1`  `L'\mcdot{}

---

Home Index