---

Step * 1 1 of Lemma polymorphic-choice-base

.....assertion..... 
1. f : ⋂A:Type. (A ⟶ A ⟶ A)
⊢ ∀x,y:Base.  (↓((f x y) = x ∈ Base) ∨ ((f x y) = y ∈ Base))
BY
{ (Auto THEN IsectHD ⌜{z:Base| (z = x ∈ Base) ∨ (z = y ∈ Base)} ⌝ 1⋅) }

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)} 
⊢ ↓((f x y) = x ∈ Base) ∨ ((f x y) = y ∈ Base)

---

Latex:

---

Latex:
.....assertion..... 
1.  f  :  \mcap{}A:Type.  (A  {}\mrightarrow{}  A  {}\mrightarrow{}  A)
\mvdash{}  \mforall{}x,y:Base.    (\mdownarrow{}((f  x  y)  =  x)  \mvee{}  ((f  x  y)  =  y))


By

---

Latex:
(Auto  THEN  IsectHD  \mkleeneopen{}\{z:Base|  (z  =  x)  \mvee{}  (z  =  y)\}  \mkleeneclose{}  1\mcdot{})

---

Home Index