---

Step * of Lemma flip_identity

∀[k:ℕ]. ∀[i,j:ℕk].  (i, j) = (λx.x) ∈ (ℕk ⟶ ℕk) supposing i = j ∈ ℤ
BY
{ (Unfold `flip` 0 THEN Auto THEN (Ext THEN Reduce 0) THEN Auto THEN RepeatFor 2 ((SplitOnConclITE THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[i,j:\mBbbN{}k].    (i,  j)  =  (\mlambda{}x.x)  supposing  i  =  j


By

---

Latex:
(Unfold  `flip`  0
  THEN  Auto
  THEN  (Ext  THEN  Reduce  0)
  THEN  Auto
  THEN  RepeatFor  2  ((SplitOnConclITE  THEN  Auto)))

---

Home Index