---

Step * 1 2 of Lemma permutation-filter


1. [A] : Type
2. u : A
3. v : A List
4. permutation(A;[];[u / v])
5. p : A ⟶ 𝔹
⊢ permutation({a:A| ↑(p a)} ;[];if p u then [u / filter(p;v)] else filter(p;v) fi )
BY
{ ((FLemma `permutation-length` [-2] THENA Auto) THEN Reduce (-1) THEN Auto') }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  u  :  A
3.  v  :  A  List
4.  permutation(A;[];[u  /  v])
5.  p  :  A  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  permutation(\{a:A|  \muparrow{}(p  a)\}  ;[];if  p  u  then  [u  /  filter(p;v)]  else  filter(p;v)  fi  )


By

---

Latex:
((FLemma  `permutation-length`  [-2]  THENA  Auto)  THEN  Reduce  (-1)  THEN  Auto')

---

Home Index