---

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


1. x : Base
2. y : Base
3. z : Base@i
4. x =a y ~ inl z@i
⊢ x = y ∈ Base
BY
{ Assert ⌜(x =a y)↓⌝⋅ }

1
.....assertion..... 
1. x : Base
2. y : Base
3. z : Base@i
4. x =a y ~ inl z@i
⊢ (x =a y)↓

2
1. x : Base
2. y : Base
3. z : Base@i
4. x =a y ~ inl z@i
5. (x =a y)↓
⊢ x = y ∈ Base

---

Latex:

---

Latex:

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


By

---

Latex:
Assert  \mkleeneopen{}(x  =a  y)\mdownarrow{}\mkleeneclose{}\mcdot{}

---

Home Index