---

Step * 1 1 of Lemma decidable__atom_equal_1


1. a : Atom1@i
2. b : Atom1@i
⊢ if a=1 b
   then inl Ax
   else (inr (λx.x) ) ∈ (a = b ∈ Atom1) ∨ (¬(a = b ∈ Atom1))
BY
{ Unfold `member` 0
THEN Refine_atomn_eqEquality `v'
THEN Auto
THEN Try (Unfold `member` 0)
THEN Try Refine_atomnEquality⋅⋅ }

1
1. a : Atom1@i
2. b : Atom1@i
3. v : (a = b ∈ Atom1) ⟶ Void
4. x : a = b ∈ Atom1@i
⊢ x = x ∈ False

---

Latex:

---

Latex:

1.  a  :  Atom1@i
2.  b  :  Atom1@i
\mvdash{}  if  a=1  b
      then  inl  Ax
      else  (inr  (\mlambda{}x.x)  )  \mmember{}  (a  =  b)  \mvee{}  (\mneg{}(a  =  b))


By

---

Latex:
Unfold  `member`  0
THEN  Refine\_atomn\_eqEquality  `v'
THEN  Auto
THEN  Try  (Unfold  `member`  0)
THEN  Try  Refine\_atomnEquality\mcdot{}\mcdot{}

---

Home Index