---

Step * 1 of Lemma split-by-indices


1. [T] : Type
2. L : T List
3. ids : ℕ List
⊢ permutation(T;L;(fst(index-split(L;ids))) @ (snd(index-split(L;ids))))
BY
{ ((InstLemma `index-split-permutation` [⌜T⌝;⌜L⌝;⌜ids⌝]⋅ THENA Auto)⋅ THEN MoveToConcl (-1)) }

1
1. [T] : Type
2. L : T List
3. ids : ℕ List
⊢ let L1,L2 = index-split(L;ids) 
  in permutation(T;L;L1 @ L2)
⇒ permutation(T;L;(fst(index-split(L;ids))) @ (snd(index-split(L;ids))))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L  :  T  List
3.  ids  :  \mBbbN{}  List
\mvdash{}  permutation(T;L;(fst(index-split(L;ids)))  @  (snd(index-split(L;ids))))


By

---

Latex:
((InstLemma  `index-split-permutation`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}ids\mkleeneclose{}]\mcdot{}  THENA  Auto)\mcdot{}  THEN  MoveToConcl  (-1))

---

Home Index