---

Step * 1 1 of Lemma split-by-indices


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))))
BY
{ xxx(RepUR ``index-split let`` 0 THEN Auto)xxx }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L  :  T  List
3.  ids  :  \mBbbN{}  List
\mvdash{}  let  L1,L2  =  index-split(L;ids) 
    in  permutation(T;L;L1  @  L2)
{}\mRightarrow{}  permutation(T;L;(fst(index-split(L;ids)))  @  (snd(index-split(L;ids))))


By

---

Latex:
xxx(RepUR  ``index-split  let``  0  THEN  Auto)xxx

---

Home Index