---

Step * of Lemma permute_list_select

∀[T:Type]. ∀[L:T List]. ∀[f:ℕ||L|| ⟶ ℕ||L||]. ∀[i:ℕ||L||].  ((L o f)[i] = L[f i] ∈ T)
BY
{ (Auto
   THEN Unfold `permute_list` 0
   THEN (InstLemma `mklist_select` [⌜T⌝;⌜||L||⌝]⋅ THENA Auto)
   THEN (RWO "-1" 0 THEN Reduce 0)
   THEN Auto') }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  Unfold  `permute\_list`  0
  THEN  (InstLemma  `mklist\_select`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}||L||\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0  THEN  Reduce  0)
  THEN  Auto')

---

Home Index