---

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

.....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
BY
{ ((Assert ↓((f 1 y) = 1 ∈ Base) ∨ ((f 1 y) = y ∈ Base) BY
          Auto)
   THEN RepeatFor 2 (D -1)
   THEN Try (Trivial)
   THEN (InstLemma `type-with-y=n` [⌜0⌝;⌜1⌝;⌜y⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN (Assert f ∈ T ⟶ T ⟶ T BY
               Auto)
   THEN (Assert (f 1 0) = (f 1 y) ∈ T BY
               RepeatFor 2 ((EqCD THEN Try (Eq))))
   THEN HypSubst' 8 (-1)
   THEN HypSubst' 10 (-1)
   THEN (D -3 THENA Auto)
   THEN HypSubst' (-1) 0
   THEN Auto) }

---

Latex:

---

Latex:
.....aux..... 
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)))
6.  1  =  1
7.  \mforall{}x,y:\mBbbZ{}.    ((f  x  y)  =  y)
8.  (f  1  0)  =  0
9.  y  :  Base
\mvdash{}  (f  1  y)  =  y


By

---

Latex:
((Assert  \mdownarrow{}((f  1  y)  =  1)  \mvee{}  ((f  1  y)  =  y)  BY
                Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  Try  (Trivial)
  THEN  (InstLemma  `type-with-y=n`  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (Assert  f  \mmember{}  T  {}\mrightarrow{}  T  {}\mrightarrow{}  T  BY
                          Auto)
  THEN  (Assert  (f  1  0)  =  (f  1  y)  BY
                          RepeatFor  2  ((EqCD  THEN  Try  (Eq))))
  THEN  HypSubst'  8  (-1)
  THEN  HypSubst'  10  (-1)
  THEN  (D  -3  THENA  Auto)
  THEN  HypSubst'  (-1)  0
  THEN  Auto)

---

Home Index