---

Step * 1 of Lemma base_sq


1. x : Base
2. y : Base
3. x = y ∈ Base
⊢ x ~ y
BY
{ TACTIC:Refine_sqequalBase THEN Auto }

---

Latex:

---

Latex:

1.  x  :  Base
2.  y  :  Base
3.  x  =  y
\mvdash{}  x  \msim{}  y


By

---

Latex:
TACTIC:Refine\_sqequalBase  THEN  Auto

---

Home Index