---

Step * 1 2 of Lemma polymorphic-choice-base


1. f : ⋂A:Type. (A ⟶ A ⟶ A)
2. ∀x,y:Base.  (↓((f x y) = x ∈ Base) ∨ ((f x y) = y ∈ Base))
⊢ (∀x,y:Base.  ((f x y) = x ∈ Base)) ∨ (∀x,y:Base.  ((f x y) = y ∈ Base))
BY
{ (Assert ∀z:Base. ((f z z) = z ∈ Base) BY
         (ParallelLast THEN D -1 With ⌜z⌝  THEN Auto THEN D -1 THEN Trivial)) }

1
1. f : ⋂A:Type. (A ⟶ A ⟶ A)
2. ∀x,y:Base.  (↓((f x y) = x ∈ Base) ∨ ((f x y) = y ∈ Base))
3. ∀z:Base. ((f z z) = z ∈ Base)
⊢ (∀x,y:Base.  ((f x y) = x ∈ Base)) ∨ (∀x,y:Base.  ((f x y) = y ∈ Base))

---

Latex:

---

Latex:

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


By

---

Latex:
(Assert  \mforall{}z:Base.  ((f  z  z)  =  z)  BY
              (ParallelLast  THEN  D  -1  With  \mkleeneopen{}z\mkleeneclose{}    THEN  Auto  THEN  D  -1  THEN  Trivial))

---

Home Index