---

Step * 2 1 1 2 1 1 of Lemma permute-to-front-permutation


1. T : Type
2. L : T List
3. idxs : ℕ List
⊢ no_repeats(ℕ||L||;filter(λi.int-list-member(i;idxs);upto(||L||)) @ filter(λi.(¬bint-list-member(i;idxs));upto(||L||)))
BY
{ (BLemma `no_repeats_append_iff`
   THEN Auto
   THEN Try ((BLemma `no_repeats_filter` THEN Auto THEN (BLemma `no_repeats_upto` THEN Auto)⋅))) }

1
1. T : Type
2. L : T List
3. idxs : ℕ List
⊢ l_disjoint(ℕ||L||;filter(λi.int-list-member(i;idxs);upto(||L||));filter(λi.(¬bint-list-member(i;idxs));upto(||L||)))

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  idxs  :  \mBbbN{}  List
\mvdash{}  no\_repeats(\mBbbN{}||L||;filter(\mlambda{}i.int-list-member(i;idxs);upto(||L||))
@  filter(\mlambda{}i.(\mneg{}\msubb{}int-list-member(i;idxs));upto(||L||)))


By

---

Latex:
(BLemma  `no\_repeats\_append\_iff`
  THEN  Auto
  THEN  Try  ((BLemma  `no\_repeats\_filter`  THEN  Auto  THEN  (BLemma  `no\_repeats\_upto`  THEN  Auto)\mcdot{})))

---

Home Index