---

Step * 1 1 1 of Lemma polymorphic-choice-base


1. f : ⋂A:Type. (A ⟶ A ⟶ A)
2. x : Base
3. y : Base
4. f ∈ {z:Base| (z = x ∈ Base) ∨ (z = y ∈ Base)} 
   ⟶ {z:Base| (z = x ∈ Base) ∨ (z = y ∈ Base)} 
   ⟶ {z:Base| (z = x ∈ Base) ∨ (z = y ∈ Base)} 
⊢ ↓((f x y) = x ∈ Base) ∨ ((f x y) = y ∈ Base)
BY
{ (Assert f x y ∈ {z:Base| (z = x ∈ Base) ∨ (z = y ∈ Base)}  BY
         Auto) }

1
1. f : ⋂A:Type. (A ⟶ A ⟶ A)
2. x : Base
3. y : Base
4. f ∈ {z:Base| (z = x ∈ Base) ∨ (z = y ∈ Base)} 
   ⟶ {z:Base| (z = x ∈ Base) ∨ (z = y ∈ Base)} 
   ⟶ {z:Base| (z = x ∈ Base) ∨ (z = y ∈ Base)} 
5. f x y ∈ {z:Base| (z = x ∈ Base) ∨ (z = y ∈ Base)} 
⊢ ↓((f x y) = x ∈ Base) ∨ ((f x y) = y ∈ Base)

---

Latex:

---

Latex:

1.  f  :  \mcap{}A:Type.  (A  {}\mrightarrow{}  A  {}\mrightarrow{}  A)
2.  x  :  Base
3.  y  :  Base
4.  f  \mmember{}  \{z:Base|  (z  =  x)  \mvee{}  (z  =  y)\}    {}\mrightarrow{}  \{z:Base|  (z  =  x)  \mvee{}  (z  =  y)\}    {}\mrightarrow{}  \{z:Base|  (z  =  x)  \mvee{}  (z  =  y)\} 
\mvdash{}  \mdownarrow{}((f  x  y)  =  x)  \mvee{}  ((f  x  y)  =  y)


By

---

Latex:
(Assert  f  x  y  \mmember{}  \{z:Base|  (z  =  x)  \mvee{}  (z  =  y)\}    BY
              Auto)

---

Home Index