---

Step * of Lemma polymorphic-choice-base

∀f:⋂A:Type. (A ⟶ A ⟶ A). ((∀x,y:Base.  ((f x y) = x ∈ Base)) ∨ (∀x,y:Base.  ((f x y) = y ∈ Base)))
BY
{ Auto }

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

---

Latex:

---

Latex:
\mforall{}f:\mcap{}A:Type.  (A  {}\mrightarrow{}  A  {}\mrightarrow{}  A).  ((\mforall{}x,y:Base.    ((f  x  y)  =  x))  \mvee{}  (\mforall{}x,y:Base.    ((f  x  y)  =  y)))


By

---

Latex:
Auto

---

Home Index