---

Step * of Lemma sqntype_list

∀[A:Type]. ∀[n:ℕ].  sqntype(n;A List) supposing sqntype(n;A)
BY
{ Auto }

1
1. A : Type
2. n : ℕ
3. sqntype(n;A)
⊢ sqntype(n;A List)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[n:\mBbbN{}].    sqntype(n;A  List)  supposing  sqntype(n;A)


By

---

Latex:
Auto

---

Home Index