---

Step * 3 of Lemma length-one-iff


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 ∈ ℤ
BY
{ ((DVar `L' THEN All Reduce THEN Auto) THEN DVar `v' THEN All Reduce THEN Auto') }

1
1. T : Type
2. u : T
3. u1 : T
4. v : T List
5. ∀[x,y:T].  (x = y ∈ T) supposing ((y ∈ [u; [u1 / v]]) and (x ∈ [u; [u1 / v]]))
6. no_repeats(T;[u; [u1 / v]])
7. 0 < (||v|| + 1) + 1
⊢ ((||v|| + 1) + 1) = 1 ∈ ℤ

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  \mforall{}[x,y:T].    (x  =  y)  supposing  ((y  \mmember{}  L)  and  (x  \mmember{}  L))
4.  no\_repeats(T;L)
5.  0  <  ||L||
\mvdash{}  ||L||  =  1


By

---

Latex:
((DVar  `L'  THEN  All  Reduce  THEN  Auto)  THEN  DVar  `v'  THEN  All  Reduce  THEN  Auto')

---

Home Index