---

Step * of Lemma base_sq

SQType(Base)
BY
{ (Unfold `sq_type` 0 THEN (UnivCD THENW Auto)) }

1
1. x : Base
2. y : Base
3. x = y ∈ Base
⊢ x ~ y

---

Latex:

---

Latex:
SQType(Base)


By

---

Latex:
(Unfold  `sq\_type`  0  THEN  (UnivCD  THENW  Auto))

---

Home Index