---

Step * 1 1 of Lemma last-decidable


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
BY
{ (((GenConclAtAddr [2; 2; 1]) THENA Auto)
   THEN D -2
   THEN Reduce 0
   THEN ((GenConclAtAddr [2; 3; 1]) THENA Auto)
   THEN D -2
   THEN Reduce 0
   THEN (All (Unfold `so_apply`))
   THEN Auto
   THEN ThinTrivial
   THEN ∀h:hyp. (D h THEN Trivial) ) }

---

Latex:

---

Latex:

1.  es  :  EO@i'
2.  e  :  E@i
3.  [P]  :  \{a:E|  loc(a)  =  loc(e)\}    {}\mrightarrow{}  \mBbbP{}
4.  f  :  \mforall{}a:\{a:E|  loc(a)  =  loc(e)\}  .  Dec(P[a])@i
5.  a  :  \{a:E|  loc(a)  =  loc(e)\}  @i
6.  b  :  \{a:E|  loc(a)  =  loc(e)\}  @i
\mvdash{}  P  a  \mLeftarrow{}{}\mRightarrow{}  P  b  \mLeftarrow{}{}\mRightarrow{}  case  f  a  of  inl(x)  =>  tt  |  inr(x)  =>  ff  =  case  f  b  of  inl(x)  =>  tt  |  inr(x)  =>  ff


By

---

Latex:
(((GenConclAtAddr  [2;  2;  1])  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0
  THEN  ((GenConclAtAddr  [2;  3;  1])  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0
  THEN  (All  (Unfold  `so\_apply`))
  THEN  Auto
  THEN  ThinTrivial
  THEN  \mforall{}h:hyp.  (D  h  THEN  Trivial)  )

---

Home Index