---

Step * 1 of Lemma rotate-by-injection


1. n : ℕ
2. i : ℕ
⊢ Inj(ℕn;ℕn;rot(n)^i)
BY
{ (BLemma `fun_exp-injection` THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  i  :  \mBbbN{}
\mvdash{}  Inj(\mBbbN{}n;\mBbbN{}n;rot(n)\^{}i)


By

---

Latex:
(BLemma  `fun\_exp-injection`  THEN  Auto)

---

Home Index