---

Step * 1 2 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
⊢ ↑x =a y
BY
{ HypSubst (-4) 0 }

1
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)

---

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{}x  =a  y


By

---

Latex:
HypSubst  (-4)  0

---

Home Index