---

Step * of Lemma permutation-sign-id

∀[n:ℕ]. (permutation-sign(n;λx.x) ~ 1)
BY
{ (InductionOnNat THEN RepUR ``permutation-sign`` 0) }

1
1. n : ℤ
⊢ 1 ~ 1

2
1. n : ℤ
2. 0 < n
3. permutation-sign(n - 1;λx.x) ~ 1
⊢ Π(Π(sign(j - i) | i < j) | j < n) ~ 1

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  (permutation-sign(n;\mlambda{}x.x)  \msim{}  1)


By

---

Latex:
(InductionOnNat  THEN  RepUR  ``permutation-sign``  0)

---

Home Index