---

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


1. x : Base
2. y : Base
3. z : Base@i
4. x =a y ~ inl z@i
5. (if x=y then tt else ff fi )↓
6. x ∈ Atom
7. y ∈ Atom
⊢ ↑(inl z)
BY
{ (RepUR ``assert`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  Base
2.  y  :  Base
3.  z  :  Base@i
4.  x  =a  y  \msim{}  inl  z@i
5.  (if  x=y  then  tt  else  ff  fi  )\mdownarrow{}
6.  x  \mmember{}  Atom
7.  y  \mmember{}  Atom
\mvdash{}  \muparrow{}(inl  z)


By

---

Latex:
(RepUR  ``assert``  0  THEN  Auto)

---

Home Index