Step
*
of Lemma
polymorphic-choice-base-sq
∀f:Base. ((f ∈ ⋂A:Type. (A ⟶ A ⟶ A))
⇒ ((f ~ λx.if f x is lambda then λy.x otherwise ⊥) ∨ (f ~ λx,y. y)))
BY
{ ((UnivCD THENA Auto) THEN (InstLemma `polymorphic-choice-base` [⌜f⌝]⋅ THENA Auto) THEN ParallelLast') }
1
1. f : Base
2. f ∈ ⋂A:Type. (A ⟶ A ⟶ A)
3. ∀x,y:Base. ((f x y) = x ∈ Base)
⊢ f ~ λx.if f x is lambda then λy.x otherwise ⊥
2
1. f : Base
2. f ∈ ⋂A:Type. (A ⟶ A ⟶ A)
3. ∀x,y:Base. ((f x y) = y ∈ Base)
⊢ f ~ λx,y. y
Latex:
Latex:
\mforall{}f:Base
((f \mmember{} \mcap{}A:Type. (A {}\mrightarrow{} A {}\mrightarrow{} A)) {}\mRightarrow{} ((f \msim{} \mlambda{}x.if f x is lambda then \mlambda{}y.x otherwise \mbot{}) \mvee{} (f \msim{} \mlambda{}x,y. y))\000C)
By
Latex:
((UnivCD THENA Auto)
THEN (InstLemma `polymorphic-choice-base` [\mkleeneopen{}f\mkleeneclose{}]\mcdot{} THENA Auto)
THEN ParallelLast')
Home
Index