---

Step * 1 of Lemma polymorphic-choice-int

.....assertion..... 
1. f : ⋂A:Type. (A ⟶ A ⟶ A)
⊢ ∀x,y:Base.  (↓((f x y) = x ∈ Base) ∨ ((f x y) = y ∈ Base))
BY
{ (Auto
   THEN (Assert 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)}  BY
               Auto)
   THEN (GenConcl ⌜(f x y) = z ∈ {z:Base| (z = x ∈ Base) ∨ (z = y ∈ Base)} ⌝⋅ THENA Auto)
   THEN D -2
   THEN D 0
   THEN Auto) }

---

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  (Assert  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)\}    BY
                          Auto)
  THEN  (GenConcl  \mkleeneopen{}(f  x  y)  =  z\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  D  0
  THEN  Auto)

---

Home Index