---

Step * 1 of Lemma last-decidable

.....assertion..... 
1. es : EO@i'
2. e : E@i
3. [P] : {a:E| loc(a) = loc(e) ∈ Id}  ─→ ℙ
4. ∀a:{a:E| loc(a) = loc(e) ∈ Id} . Dec(P[a])@i
⊢ ∃f:{a:E| loc(a) = loc(e) ∈ Id}  ─→ 𝔹. ∀a,b:{a:E| loc(a) = loc(e) ∈ Id} .  (P[a] ⇐⇒ P[b] ⇐⇒ f[a] = f[b])
BY
{ ((RenameVar `f' (-1))
   THEN ((InstConcl [⌈λa.case f a of inl(x) => tt | inr(x) => ff⌉])⋅ THENA (Auto THEN DoSubsume THEN Auto))
   THEN RepUR ``so_apply`` 0
   THEN RepeatFor 2 ((D 0 THENA Auto))) }

1
1. es : EO@i'
2. e : E@i
3. [P] : {a:E| loc(a) = loc(e) ∈ Id}  ─→ ℙ
4. f : ∀a:{a:E| loc(a) = loc(e) ∈ Id} . Dec(P[a])@i
5. a : {a:E| loc(a) = loc(e) ∈ Id} @i
6. b : {a:E| loc(a) = loc(e) ∈ Id} @i
⊢ P a ⇐⇒ P b ⇐⇒ case f a of inl(x) => tt | inr(x) => ff = case f b of inl(x) => tt | inr(x) => ff

---

Latex:


.....assertion..... 
1.  es  :  EO@i'
2.  e  :  E@i
3.  [P]  :  \{a:E|  loc(a)  =  loc(e)\}    {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}a:\{a:E|  loc(a)  =  loc(e)\}  .  Dec(P[a])@i
\mvdash{}  \mexists{}f:\{a:E|  loc(a)  =  loc(e)\}    {}\mrightarrow{}  \mBbbB{}.  \mforall{}a,b:\{a:E|  loc(a)  =  loc(e)\}  .    (P[a]  \mLeftarrow{}{}\mRightarrow{}  P[b]  \mLeftarrow{}{}\mRightarrow{}  f[a]  =  f[b])


By

((RenameVar  `f'  (-1))
  THEN  ((InstConcl  [\mkleeneopen{}\mlambda{}a.case  f  a  of  inl(x)  =>  tt  |  inr(x)  =>  ff\mkleeneclose{}])\mcdot{}
              THENA  (Auto  THEN  DoSubsume  THEN  Auto)
              )
  THEN  RepUR  ``so\_apply``  0
  THEN  RepeatFor  2  ((D  0  THENA  Auto)))

---

Home Index