---

Step * of Lemma cons-ndlist

∀[T:Type]. ∀[L:ndlist(T)]. ∀[x:T].  [x / L] ∈ ndlist(T) supposing ¬(x ∈ L)
BY
{ Auto }

1
1. T : Type
2. L : ndlist(T)
3. x : T
4. ¬(x ∈ L)
⊢ [x / L] ∈ ndlist(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:ndlist(T)].  \mforall{}[x:T].    [x  /  L]  \mmember{}  ndlist(T)  supposing  \mneg{}(x  \mmember{}  L)


By

---

Latex:
Auto

---

Home Index