---

Step * 1 1 1 of Lemma extend_perm_over_id


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)
BY
{ ((AbReduce 0 THEN RWH (LemmaC `extend_permf_over_id`) 0) THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((AbReduce  0  THEN  RWH  (LemmaC  `extend\_permf\_over\_id`)  0)  THEN  Auto)

---

Home Index