---

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


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)
BY
{ (Reduce 0 THEN GenHypAtAddr 0 [1;1]  THEN DVar `v' THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbP{}
3.  g  :  \mforall{}t:T.  ((P  t)  \mvee{}  (\mneg{}(P  t)))@i
4.  t  :  T@i
5.  P  t@i
\mvdash{}  \muparrow{}isl(g  t)


By

---

Latex:
(Reduce  0  THEN  GenHypAtAddr  0  [1;1]    THEN  DVar  `v'  THEN  Auto)\mcdot{}

---

Home Index