---

Step * 1 1 of Lemma sq-decider-atom-deq

.....assertion..... 
1. x : Base
2. y : Base
3. z : Base@i
4. x =a y ~ inl z@i
⊢ (x =a y)↓
BY
{ (HypSubst (-1) 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  x  :  Base
2.  y  :  Base
3.  z  :  Base@i
4.  x  =a  y  \msim{}  inl  z@i
\mvdash{}  (x  =a  y)\mdownarrow{}


By

---

Latex:
(HypSubst  (-1)  0  THEN  Reduce  0  THEN  Auto)

---

Home Index