---

Step * 1 2 1 1 3 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))
3. ∀z:Base. ((f z z) = z ∈ Base)
4. ((f 0 1) = 0 ∈ Base) ∨ ((f 0 1) = 1 ∈ Base)
5. ((f 0 1) = 0 ∈ Base) ⇒ ((∀y:Base. ((f 1 y) = 1 ∈ Base)) ∧ (∀x:Base. ((f x 0) = x ∈ Base)))
⊢ (∀x,y:Base.  ((f x y) = x ∈ Base)) ∨ (∀x,y:Base.  ((f x y) = y ∈ Base))
BY
{ (Assert ((f 0 1) = 1 ∈ Base) ⇒ ((∀y:Base. ((f 1 y) = y ∈ Base)) ∧ (∀x:Base. ((f x 0) = 0 ∈ Base))) BY
         ((D 0 THENA ((Assert f ∈ Base ⟶ Base ⟶ Base BY Auto) THEN Auto))
          THEN (InstLemma `polymorphic-choice-int` [⌜f⌝]⋅ THENA Auto)
          THEN D -1
          THEN (RWO "-1" (-2) THENA Auto)
          THEN (((Assert 0 = 1 ∈ ℤ BY (HypSubst' (-2) 0 THEN Complete (Auto))) THEN TrivialArith)
          ORELSE (InstHyp [⌜1⌝;⌜0⌝] (-1)⋅ THEN Auto)
          ))) }

1
.....aux..... 
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)
4. ((f 0 1) = 0 ∈ Base) ∨ ((f 0 1) = 1 ∈ Base)
5. ((f 0 1) = 0 ∈ Base) ⇒ ((∀y:Base. ((f 1 y) = 1 ∈ Base)) ∧ (∀x:Base. ((f x 0) = x ∈ Base)))
6. 1 = 1 ∈ Base
7. ∀x,y:ℤ.  ((f x y) = y ∈ ℤ)
8. (f 1 0) = 0 ∈ ℤ
9. y : Base
⊢ (f 1 y) = y ∈ Base

2
.....aux..... 
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)
4. ((f 0 1) = 0 ∈ Base) ∨ ((f 0 1) = 1 ∈ Base)
5. ((f 0 1) = 0 ∈ Base) ⇒ ((∀y:Base. ((f 1 y) = 1 ∈ Base)) ∧ (∀x:Base. ((f x 0) = x ∈ Base)))
6. 1 = 1 ∈ Base
7. ∀x,y:ℤ.  ((f x y) = y ∈ ℤ)
8. (f 1 0) = 0 ∈ ℤ
9. ∀y:Base. ((f 1 y) = y ∈ Base)
10. x : Base
⊢ (f x 0) = 0 ∈ Base

3
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)
4. ((f 0 1) = 0 ∈ Base) ∨ ((f 0 1) = 1 ∈ Base)
5. ((f 0 1) = 0 ∈ Base) ⇒ ((∀y:Base. ((f 1 y) = 1 ∈ Base)) ∧ (∀x:Base. ((f x 0) = x ∈ Base)))
6. ((f 0 1) = 1 ∈ Base) ⇒ ((∀y:Base. ((f 1 y) = y ∈ Base)) ∧ (∀x:Base. ((f x 0) = 0 ∈ 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))
3.  \mforall{}z:Base.  ((f  z  z)  =  z)
4.  ((f  0  1)  =  0)  \mvee{}  ((f  0  1)  =  1)
5.  ((f  0  1)  =  0)  {}\mRightarrow{}  ((\mforall{}y:Base.  ((f  1  y)  =  1))  \mwedge{}  (\mforall{}x:Base.  ((f  x  0)  =  x)))
\mvdash{}  (\mforall{}x,y:Base.    ((f  x  y)  =  x))  \mvee{}  (\mforall{}x,y:Base.    ((f  x  y)  =  y))


By

---

Latex:
(Assert  ((f  0  1)  =  1)  {}\mRightarrow{}  ((\mforall{}y:Base.  ((f  1  y)  =  y))  \mwedge{}  (\mforall{}x:Base.  ((f  x  0)  =  0)))  BY
              ((D  0  THENA  ((Assert  f  \mmember{}  Base  {}\mrightarrow{}  Base  {}\mrightarrow{}  Base  BY  Auto)  THEN  Auto))
                THEN  (InstLemma  `polymorphic-choice-int`  [\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  D  -1
                THEN  (RWO  "-1"  (-2)  THENA  Auto)
                THEN  (((Assert  0  =  1  BY  (HypSubst'  (-2)  0  THEN  Complete  (Auto)))  THEN  TrivialArith)
                ORELSE  (InstHyp  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)
                )))

---

Home Index