---

Step * of Lemma length-one-iff

∀[T:Type]. ∀[L:T List].
  uiff(||L|| = 1 ∈ ℤ;(∀[x,y:T].  (x = y ∈ T) supposing ((y ∈ L) and (x ∈ L))) ∧ no_repeats(T;L) ∧ 0 < ||L||)
BY
{ Auto }

1
1. T : Type
2. L : T List
3. ||L|| = 1 ∈ ℤ
4. x : T
5. y : T
6. (x ∈ L)
7. (y ∈ L)
⊢ x = y ∈ T

2
1. T : Type
2. L : T List
3. ||L|| = 1 ∈ ℤ
⊢ no_repeats(T;L)

3
1. T : Type
2. L : T List
3. ∀[x,y:T].  (x = y ∈ T) supposing ((y ∈ L) and (x ∈ L))
4. no_repeats(T;L)
5. 0 < ||L||
⊢ ||L|| = 1 ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].
    uiff(||L||  =  1;(\mforall{}[x,y:T].    (x  =  y)  supposing  ((y  \mmember{}  L)  and  (x  \mmember{}  L)))  \mwedge{}  no\_repeats(T;L)  \mwedge{}  0  <  ||L||)


By

---

Latex:
Auto

---

Home Index