---

Step * of Lemma permutation-singleton

∀[T:Type]. ∀[x:T]. ∀[ts:T List].  ts = [x] ∈ (T List) supposing permutation(T;[x];ts)
BY
{ (Auto
   THEN FLemma `permutation-length` [-1]
   THEN Auto
   THEN RepeatFor 2 ((D -3 THEN Reduce (-1) THEN Auto'))
   THEN EqCD
   THEN Auto
   THEN Thin (-1)) }

1
1. T : Type
2. x : T
3. u : T
4. permutation(T;[x];[u])
⊢ u = x ∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].  \mforall{}[ts:T  List].    ts  =  [x]  supposing  permutation(T;[x];ts)


By

---

Latex:
(Auto
  THEN  FLemma  `permutation-length`  [-1]
  THEN  Auto
  THEN  RepeatFor  2  ((D  -3  THEN  Reduce  (-1)  THEN  Auto'))
  THEN  EqCD
  THEN  Auto
  THEN  Thin  (-1))

---

Home Index