---

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