---

Step * of Lemma list-is-singleton-iff

No Annotations
∀[T:Type]. ∀L:T List. ∀x:T.  (L = [x] ∈ (T List) ⇐⇒ no_repeats(T;L) ∧ (∀f:T. ((f ∈ L) ⇐⇒ f = x ∈ T)))
BY
{ Auto }

1
1. T : Type
2. L : T List
3. x : T
4. L = [x] ∈ (T List)
⊢ no_repeats(T;L)

2
1. T : Type
2. L : T List
3. x : T
4. L = [x] ∈ (T List)
5. f : T
6. (f ∈ L)
⊢ f = x ∈ T

3
1. [T] : Type
2. L : T List
3. x : T
4. L = [x] ∈ (T List)
5. f : T
6. f = x ∈ T
⊢ (f ∈ L)

4
1. T : Type
2. L : T List
3. x : T
4. no_repeats(T;L)
5. ∀f:T. ((f ∈ L) ⇐⇒ f = x ∈ T)
⊢ L = [x] ∈ (T List)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}x:T.    (L  =  [x]  \mLeftarrow{}{}\mRightarrow{}  no\_repeats(T;L)  \mwedge{}  (\mforall{}f:T.  ((f  \mmember{}  L)  \mLeftarrow{}{}\mRightarrow{}  f  =  x)))


By

---

Latex:
Auto

---

Home Index