---

Step * 1 1 1 1 of Lemma equipollent-split


1. [T] : Type
2. [P] : T ⟶ ℙ
3. p : x:T ⟶ (↓P[x] + (¬↓P[x]))
4. a1 : T
⊢ ∀a2:T
    ((case p a1 of inl(z) => inl a1 | inr(z) => inr a1 
    = case p a2 of inl(z) => inl a2 | inr(z) => inr a2 
    ∈ ({x:T| ↓P[x]}  + {x:T| ↓¬P[x]} ))
    ⇒ (a1 = a2 ∈ T))
BY
{ ((D 0 THENA Auto)
   THEN (GenConclAtAddr [1;2;1] THEN Thin (-1))
   THEN GenConclAtAddr [1;3;1]
   THEN Thin (-1)
   THEN D -2
   THEN D -1
   THEN (Reduce 0 THEN Auto)⋅) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [P]  :  T  {}\mrightarrow{}  \mBbbP{}
3.  p  :  x:T  {}\mrightarrow{}  (\mdownarrow{}P[x]  +  (\mneg{}\mdownarrow{}P[x]))
4.  a1  :  T
\mvdash{}  \mforall{}a2:T
        ((case  p  a1  of  inl(z)  =>  inl  a1  |  inr(z)  =>  inr  a1 
        =  case  p  a2  of  inl(z)  =>  inl  a2  |  inr(z)  =>  inr  a2  )
        {}\mRightarrow{}  (a1  =  a2))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (GenConclAtAddr  [1;2;1]  THEN  Thin  (-1))
  THEN  GenConclAtAddr  [1;3;1]
  THEN  Thin  (-1)
  THEN  D  -2
  THEN  D  -1
  THEN  (Reduce  0  THEN  Auto)\mcdot{})

---

Home Index