Step
*
1
1
1
1
of Lemma
polymorphic-choice-base
1. f : ⋂A:Type. (A ⟶ A ⟶ A)
2. x : Base
3. y : Base
4. f ∈ {z:Base| (z = x ∈ Base) ∨ (z = y ∈ Base)}
⟶ {z:Base| (z = x ∈ Base) ∨ (z = y ∈ Base)}
⟶ {z:Base| (z = x ∈ Base) ∨ (z = y ∈ Base)}
5. f x y ∈ {z:Base| (z = x ∈ Base) ∨ (z = y ∈ Base)}
⊢ ↓((f x y) = x ∈ Base) ∨ ((f x y) = y ∈ Base)
BY
{ (MemTypeHD (-1) THEN Auto) }
Latex:
Latex:
1. f : \mcap{}A:Type. (A {}\mrightarrow{} A {}\mrightarrow{} A)
2. x : Base
3. y : Base
4. f \mmember{} \{z:Base| (z = x) \mvee{} (z = y)\} {}\mrightarrow{} \{z:Base| (z = x) \mvee{} (z = y)\} {}\mrightarrow{} \{z:Base| (z = x) \mvee{} (z = y)\}
5. f x y \mmember{} \{z:Base| (z = x) \mvee{} (z = y)\}
\mvdash{} \mdownarrow{}((f x y) = x) \mvee{} ((f x y) = y)
By
Latex:
(MemTypeHD (-1) THEN Auto)
Home
Index