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