Step
*
1
of Lemma
polymorphic-choice-base
1. f : ⋂A:Type. (A ⟶ A ⟶ A)
⊢ (∀x,y:Base. ((f x y) = x ∈ Base)) ∨ (∀x,y:Base. ((f x y) = y ∈ Base))
BY
{ 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: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)
\mvdash{} (\mforall{}x,y:Base. ((f x y) = x)) \mvee{} (\mforall{}x,y:Base. ((f x y) = y))
By
Latex:
Assert \mkleeneopen{}\mforall{}x,y:Base. (\mdownarrow{}((f x y) = x) \mvee{} ((f x y) = y))\mkleeneclose{}\mcdot{}
Home
Index