Step
*
2
2
of Lemma
exists_det_fun
1. T : Type
2. A : T ⟶ ℙ
3. ∀x:T. SqStable(A x)@i
4. g : x:T ⟶ (A x + (¬(A x)))@i
5. x : T@i
6. ↑((λx.isl(g x)) x)@i
⊢ A x
BY
{ (Reduce (-1) THEN MoveToConcl (-1) THEN GenConclAtAddr [1;1;1] THEN D -2 THEN Reduce 0 THEN Auto) }
Latex:
Latex:
1. T : Type
2. A : T {}\mrightarrow{} \mBbbP{}
3. \mforall{}x:T. SqStable(A x)@i
4. g : x:T {}\mrightarrow{} (A x + (\mneg{}(A x)))@i
5. x : T@i
6. \muparrow{}((\mlambda{}x.isl(g x)) x)@i
\mvdash{} A x
By
Latex:
(Reduce (-1) THEN MoveToConcl (-1) THEN GenConclAtAddr [1;1;1] THEN D -2 THEN Reduce 0 THEN Auto)
Home
Index