---

Step * of Lemma extend_perm_over_itcomp

∀n:ℕ. ∀ps:Sym(n) List.  (↑{n}(Π ps) = (Π map(λp.↑{n}(p);ps)) ∈ Sym(n + 1))
BY
{ ((UnivCD THENM ListInd (-1)) THENA Auto) }

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

2
1. n : ℕ
2. u : Sym(n)
3. v : Sym(n) List
4. ↑{n}(Π v) = (Π map(λp.↑{n}(p);v)) ∈ Sym(n + 1)
⊢ ↑{n}(Π [u / v]) = (Π map(λp.↑{n}(p);[u / v])) ∈ Sym(n + 1)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}ps:Sym(n)  List.    (\muparrow{}\{n\}(\mPi{}  ps)  =  (\mPi{}  map(\mlambda{}p.\muparrow{}\{n\}(p);ps)))


By

---

Latex:
((UnivCD  THENM  ListInd  (-1))  THENA  Auto)

---

Home Index