---

Step * of Lemma permute_list_length

∀[T:Type]. ∀[L:T List]. ∀[f:Top].  (||(L o f)|| ~ ||L||)
BY
{ ((UnivCD THENA Auto) THEN (Unfold `permute_list` 0 THEN RWO "mklist_length" 0 THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[f:Top].    (||(L  o  f)||  \msim{}  ||L||)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (Unfold  `permute\_list`  0  THEN  RWO  "mklist\_length"  0  THEN  Auto)\mcdot{})

---

Home Index