---

Step * 1 of Lemma flip-injection


1. n : ℕ
2. i : ℕn
3. j : ℕn
4. a1 : ℕn
5. a2 : ℕn
6. ((i, j) a1) = ((i, j) a2) ∈ ℕn
⊢ a1 = a2 ∈ ℕn
BY
{ (RepUR ``flip`` (-1) THEN Repeat (∀h:hyp. (SplitOnHypITE h  THEN Auto) )) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  i  :  \mBbbN{}n
3.  j  :  \mBbbN{}n
4.  a1  :  \mBbbN{}n
5.  a2  :  \mBbbN{}n
6.  ((i,  j)  a1)  =  ((i,  j)  a2)
\mvdash{}  a1  =  a2


By

---

Latex:
(RepUR  ``flip``  (-1)  THEN  Repeat  (\mforall{}h:hyp.  (SplitOnHypITE  h    THEN  Auto)  ))

---

Home Index