---

Step * 1 1 of Lemma extend_perm_over_id


1. n : ℕ
⊢ id_perm() = ↑{n}(id_perm()) ∈ perm_sig(ℕn + 1)
BY
{ Unfolds ``id_perm extend_perm`` 0 }

1
1. n : ℕ
⊢ mk_perm(Id;Id) = mk_perm(extend_permf(mk_perm(Id;Id).f;n);extend_permf(mk_perm(Id;Id).b;n)) ∈ perm_sig(ℕn + 1)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
\mvdash{}  id\_perm()  =  \muparrow{}\{n\}(id\_perm())


By

---

Latex:
Unfolds  ``id\_perm  extend\_perm``  0

---

Home Index