Step
*
1
1
of Lemma
choicef_wf
1. xm : ∀P:ℙ. (P ∨ (¬P))
2. T : Type
3. P : T ⟶ ℙ
4. ∃a:T. P[a]
5. z : {y:T| P[y]} ∨ (¬{y:T| P[y]} )
6. (xm {y:T| P[y]} ) = z ∈ ({y:T| P[y]} ∨ (¬{y:T| P[y]} ))
⊢ case z of inl(z) => z | inr(w) => "???" ∈ T
BY
{ ((D 5 THEN Reduce 0) THEN Auto) }
1
1. xm : ∀P:ℙ. (P ∨ (¬P))
2. T : Type
3. P : T ⟶ ℙ
4. ∃a:T. P[a]
5. y : ¬{y:T| P[y]}
6. (xm {y:T| P[y]} ) = (inr y ) ∈ ({y:T| P[y]} ∨ (¬{y:T| P[y]} ))
⊢ "???" ∈ T
Latex:
Latex:
1. xm : \mforall{}P:\mBbbP{}. (P \mvee{} (\mneg{}P))
2. T : Type
3. P : T {}\mrightarrow{} \mBbbP{}
4. \mexists{}a:T. P[a]
5. z : \{y:T| P[y]\} \mvee{} (\mneg{}\{y:T| P[y]\} )
6. (xm \{y:T| P[y]\} ) = z
\mvdash{} case z of inl(z) => z | inr(w) => "???" \mmember{} T
By
Latex:
((D 5 THEN Reduce 0) THEN Auto)
Home
Index