---

Step * 1 of Lemma extract-decider-of-decidable-prop


1. [T] : Type
2. [P] : T ⟶ ℙ
3. ∀t:T. ((P t) ∨ (¬(P t)))@i
⊢ ∃f:T ⟶ 𝔹. ∀t:T. (↑(f t) ⇐⇒ P t)
BY
{ (RenameVar `g' 3 THEN InstConcl [⌜λm.isl(g m)⌝]⋅ THEN Auto THEN skip{Auto})⋅ }

1
1. [T] : Type
2. [P] : T ⟶ ℙ
3. g : ∀t:T. ((P t) ∨ (¬(P t)))@i
4. t : T@i
5. ↑((λm.isl(g m)) t)@i
⊢ P t

2
1. T : Type
2. P : T ⟶ ℙ
3. g : ∀t:T. ((P t) ∨ (¬(P t)))@i
4. t : T@i
5. P t@i
⊢ ↑isl(g t)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [P]  :  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}t:T.  ((P  t)  \mvee{}  (\mneg{}(P  t)))@i
\mvdash{}  \mexists{}f:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}t:T.  (\muparrow{}(f  t)  \mLeftarrow{}{}\mRightarrow{}  P  t)


By

---

Latex:
(RenameVar  `g'  3  THEN  InstConcl  [\mkleeneopen{}\mlambda{}m.isl(g  m)\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  skip\{Auto\})\mcdot{}

---

Home Index