---

Step * of Lemma length-one-member

∀[T:Type]. ∀[L:T List].  ∀[x,y:T].  (x = y ∈ T) supposing ((y ∈ L) and (x ∈ L)) supposing ||L|| = 1 ∈ ℤ
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN RepeatFor 2 ((D -1 THEN Reduce 0 THEN Try (Complete (Auto')))) THEN Auto) }

1
1. T : Type
2. u : T
3. 1 = 1 ∈ ℤ
4. x : T
5. y : T
6. (x ∈ [u])
7. (y ∈ [u])
⊢ x = y ∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].    \mforall{}[x,y:T].    (x  =  y)  supposing  ((y  \mmember{}  L)  and  (x  \mmember{}  L))  supposing  ||L||  =  1


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  RepeatFor  2  ((D  -1  THEN  Reduce  0  THEN  Try  (Complete  (Auto'))))
  THEN  Auto)

---

Home Index