---

Step * 1 of Lemma decidable__atom_equal_1


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

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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index