---

Step * of Lemma permute_list-identity

∀[T:Type]. ∀[L:T List].  ((L o λx.x) = L ∈ (T List))
BY
{ (Auto
   THEN BLemma `list_extensionality`
   THEN Auto
   THEN RWW "permute_list_length permute_list_select" 0
   THEN Reduce 0
   THEN Auto
   THEN RWW "permute_list_length" (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].    ((L  o  \mlambda{}x.x)  =  L)


By

---

Latex:
(Auto
  THEN  BLemma  `list\_extensionality`
  THEN  Auto
  THEN  RWW  "permute\_list\_length  permute\_list\_select"  0
  THEN  Reduce  0
  THEN  Auto
  THEN  RWW  "permute\_list\_length"  (-1)
  THEN  Auto)

---

Home Index