---

Step * of Lemma sv-list-tail

∀[A:Type]. ∀[L:A List].  0 < ||L|| ⇒ single-valued-list(tl(L);A) supposing single-valued-list(L;A)
BY
{ (Unfold `single-valued-list` 0 THEN Auto THEN BackThruSomeHyp) }

1
1. A : Type
2. L : A List
3. ∀x,y:A.  ((x ∈ L) ⇒ (y ∈ L) ⇒ (x = y ∈ A))
4. 0 < ||L||@i
5. x : A@i
6. y : A@i
7. (x ∈ tl(L))@i
8. (y ∈ tl(L))@i
⊢ (x ∈ L)

2
1. A : Type
2. L : A List
3. ∀x,y:A.  ((x ∈ L) ⇒ (y ∈ L) ⇒ (x = y ∈ A))
4. 0 < ||L||@i
5. x : A@i
6. y : A@i
7. (x ∈ tl(L))@i
8. (y ∈ tl(L))@i
⊢ (y ∈ L)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[L:A  List].    0  <  ||L||  {}\mRightarrow{}  single-valued-list(tl(L);A)  supposing  single-valued-list(L;A)


By

---

Latex:
(Unfold  `single-valued-list`  0  THEN  Auto  THEN  BackThruSomeHyp)

---

Home Index