---

Step * 1 2 1 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)
⊢ (∀x,y:Base.  ((f x y) = x ∈ Base)) ∨ (∀x,y:Base.  ((f x y) = y ∈ Base))
BY
{ ((Assert ↓((f 0 1) = 0 ∈ Base) ∨ ((f 0 1) = 1 ∈ Base) BY
          Auto)
   THEN (Assert ((f 0 1) = 0 ∈ Base) ∨ ((f 0 1) = 1 ∈ Base) BY
               (UseWitness ⌜if f 0 1=0 then inl Ax else (inr Ax )⌝⋅
                THEN RepeatFor 2 (D -1)
                THEN HypSubst' (-1) 0
                THEN Reduce 0
                THEN Auto))
   THEN Thin (-2)) }

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)
4. ((f 0 1) = 0 ∈ Base) ∨ ((f 0 1) = 1 ∈ 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)
\mvdash{}  (\mforall{}x,y:Base.    ((f  x  y)  =  x))  \mvee{}  (\mforall{}x,y:Base.    ((f  x  y)  =  y))


By

---

Latex:
((Assert  \mdownarrow{}((f  0  1)  =  0)  \mvee{}  ((f  0  1)  =  1)  BY
                Auto)
  THEN  (Assert  ((f  0  1)  =  0)  \mvee{}  ((f  0  1)  =  1)  BY
                          (UseWitness  \mkleeneopen{}if  f  0  1=0  then  inl  Ax  else  (inr  Ax  )\mkleeneclose{}\mcdot{}
                            THEN  RepeatFor  2  (D  -1)
                            THEN  HypSubst'  (-1)  0
                            THEN  Reduce  0
                            THEN  Auto))
  THEN  Thin  (-2))

---

Home Index