---

Step * 1 1 of Lemma permutation-filter


1. [A] : Type
2. permutation(A;[];[])
3. p : A ⟶ 𝔹
⊢ permutation({a:A| ↑(p a)} ;[];[])
BY
{ (BLemma `permutation_weakening` THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  permutation(A;[];[])
3.  p  :  A  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  permutation(\{a:A|  \muparrow{}(p  a)\}  ;[];[])


By

---

Latex:
(BLemma  `permutation\_weakening`  THEN  Auto)

---

Home Index