---

Step * 1 of Lemma extend_permf_over_id


1. n : ℕ
⊢ extend_permf(Id;n) = Id ∈ (ℕn + 1 ⟶ ℕn + 1)
BY
{ (Unfolds ``identity extend_permf`` 0 THEN EqCD THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
\mvdash{}  extend\_permf(Id;n)  =  Id


By

---

Latex:
(Unfolds  ``identity  extend\_permf``  0  THEN  EqCD  THEN  Reduce  0  THEN  Auto)

---

Home Index