---

Step * 1 of Lemma decidable__atom_equal_2


1. a : Atom2@i
2. b : Atom2@i
⊢ (a = b ∈ Atom2) ∨ (¬(a = b ∈ Atom2))
BY
{ UseWitness ⌜if a=2 b
               then inl Ax
               else (inr (λx.x) )⌝
⋅⋅ }

1
1. a : Atom2@i
2. b : Atom2@i
⊢ if a=2 b
   then inl Ax
   else (inr (λx.x) ) ∈ (a = b ∈ Atom2) ∨ (¬(a = b ∈ Atom2))

---

Latex:

---

Latex:

1.  a  :  Atom2@i
2.  b  :  Atom2@i
\mvdash{}  (a  =  b)  \mvee{}  (\mneg{}(a  =  b))


By

---

Latex:
UseWitness  \mkleeneopen{}if  a=2  b
                          then  inl  Ax
                          else  (inr  (\mlambda{}x.x)  )\mkleeneclose{}
\mcdot{}\mcdot{}

---

Home Index