---

Step * 1 of Lemma extend_perm_over_itcomp


1. n : ℕ
⊢ ↑{n}(Π []) = (Π map(λp.↑{n}(p);[])) ∈ Sym(n + 1)
BY
{ AbReduce 0 }

1
1. n : ℕ
⊢ ↑{n}(id_perm()) = id_perm() ∈ Sym(n + 1)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
\mvdash{}  \muparrow{}\{n\}(\mPi{}  [])  =  (\mPi{}  map(\mlambda{}p.\muparrow{}\{n\}(p);[]))


By

---

Latex:
AbReduce  0

---

Home Index