---

Step * 1 1 of Lemma extend_perm_over_itcomp


1. n : ℕ
⊢ ↑{n}(id_perm()) = id_perm() ∈ Sym(n + 1)
BY
{ (BackThruLemma `extend_perm_over_id` THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(BackThruLemma  `extend\_perm\_over\_id`  THEN  Auto)

---

Home Index