---

Step * of Lemma permute_permute_list

∀[T:Type]. ∀[L:T List]. ∀[f,g:ℕ||L|| ⟶ ℕ||L||].  (((L o f) o g) = (L o f o g) ∈ (T List))
BY
{ ((Auto
    THENM InstLemma `permute_list_length` [T;L;f]
    THENM InstLemma `permute_list_length` [T;L;f o g]
    THENM InstLemma `permute_list_length` [T;(L o f);g]
    THENM BackThruLemma `list_extensionality`
    THENM RWW "permute_list_select" 0
    THENM Reduce 0)
   THEN Auto
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[f,g:\mBbbN{}||L||  {}\mrightarrow{}  \mBbbN{}||L||].    (((L  o  f)  o  g)  =  (L  o  f  o  g))


By

---

Latex:
((Auto
    THENM  InstLemma  `permute\_list\_length`  [T;L;f]
    THENM  InstLemma  `permute\_list\_length`  [T;L;f  o  g]
    THENM  InstLemma  `permute\_list\_length`  [T;(L  o  f);g]
    THENM  BackThruLemma  `list\_extensionality`
    THENM  RWW  "permute\_list\_select"  0
    THENM  Reduce  0)
  THEN  Auto
  THEN  Auto')

---

Home Index