---

Step * 1 1 1 1 1 1 1 of Lemma sg-inv-op


1. sg : s-Group
2. v : Point
3. v ≡ (v v)
4. 1 ≡ v
⊢ v ≡ 1
BY
{ EAuto 1 }

---

Latex:

---

Latex:

1.  sg  :  s-Group
2.  v  :  Point
3.  v  \mequiv{}  (v  v)
4.  1  \mequiv{}  v
\mvdash{}  v  \mequiv{}  1


By

---

Latex:
EAuto  1

---

Home Index