---

Step * of Lemma tl_perm_wf

∀n:ℕ+. ∀p:Perm(ℕn).  (tl_perm(p) ∈ Perm(ℕ+n))
BY
{ ((UnivCD THENA Auto) THEN MemTypeCD) }

1
1. n : ℕ+
2. p : Perm(ℕn)
⊢ tl_perm(p) ∈ perm_sig(ℕ+n)

2
.....set predicate..... 
1. n : ℕ+
2. p : Perm(ℕn)
⊢ InvFuns(ℕ+n;ℕ+n;tl_perm(p).f;tl_perm(p).b)

3
.....wf..... 
1. n : ℕ+
2. p : Perm(ℕn)
3. p1 : perm_sig(ℕ+n)
⊢ istype(InvFuns(ℕ+n;ℕ+n;p1.f;p1.b))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}p:Perm(\mBbbN{}n).    (tl\_perm(p)  \mmember{}  Perm(\mBbbN{}\msupplus{}n))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  MemTypeCD)

---

Home Index