---

Step * of Lemma polymorphic-choice-int

∀f:⋂A:Type. (A ⟶ A ⟶ A). ((∀x,y:ℤ.  ((f x y) = x ∈ ℤ)) ∨ (∀x,y:ℤ.  ((f x y) = y ∈ ℤ)))
BY
{ (Auto THEN Assert ⌜∀x,y:Base.  (↓((f x y) = x ∈ Base) ∨ ((f x y) = y ∈ Base))⌝⋅) }

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

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}\mforall{}x,y:Base.    (\mdownarrow{}((f  x  y)  =  x)  \mvee{}  ((f  x  y)  =  y))\mkleeneclose{}\mcdot{})

---

Home Index