---

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


1. x : Base
2. y : Base
3. z : Base@i
4. x =a y ~ inl z@i
5. (x =a y)↓
⊢ x = y ∈ Base
BY
{ (OnHyp -1 (Unfold_o Obid: eq_atom) THEN HasValueD (-1) THEN (BLemma `assert_of_eq_atom` ⋅ THENA Auto)) }

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
⊢ ↑x =a y

---

Latex:

---

Latex:

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


By

---

Latex:
(OnHyp  -1  (Unfold\_o  Obid:  eq\_atom)
  THEN  HasValueD  (-1)
  THEN  (BLemma  `assert\_of\_eq\_atom`  \mcdot{}  THENA  Auto))

---

Home Index