Step
*
1
1
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. ↑((λm.isl(g m)) t)@i
⊢ P t
BY
{ (Reduce 5 THEN GenHypAtAddr 5 [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.  \muparrow{}((\mlambda{}m.isl(g  m))  t)@i
\mvdash{}  P  t
By
Latex:
(Reduce  5  THEN  GenHypAtAddr  5  [1;1]    THEN  DVar  `v'  THEN  Auto)\mcdot{}
Home
Index