---

Step * of Lemma compose-flips-injection

∀n:ℕ. ∀L:(ℕn × ℕn) List.  Inj(ℕn;ℕn;compose-flips(L))
BY
{ (InductionOnList THEN Try (DVar `u') THEN RepUR ``compose-flips`` 0 THEN Try (Fold `compose-flips` 0) THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}L:(\mBbbN{}n  \mtimes{}  \mBbbN{}n)  List.    Inj(\mBbbN{}n;\mBbbN{}n;compose-flips(L))


By

---

Latex:
(InductionOnList
  THEN  Try  (DVar  `u')
  THEN  RepUR  ``compose-flips``  0
  THEN  Try  (Fold  `compose-flips`  0)
  THEN  EAuto  1)

---

Home Index