---

Step * of Lemma polymorphic-choice

∀f:⋂A:Type. (A ⟶ A ⟶ A). ((f = (λx,y. x) ∈ (⋂A:Type. (A ⟶ A ⟶ A))) ∨ (f = (λx,y. y) ∈ (⋂A:Type. (A ⟶ A ⟶ A))))
BY
{ (InstLemma `polymorphic-choice-base` []
   THEN RepeatFor 2 (ParallelLast')
   THEN (EqTypeCD THENA Auto)
   THEN RepeatFor 2 ((FunExt THENA Auto))
   THEN Reduce 0
   THEN (PointwiseFunctionalityForEquality (-2) THENA Auto)
   THEN (PointwiseFunctionalityForEquality (-1) THENA Auto)
   THEN (RWO "2" 0 THEN Auto)
   THEN (Unfold `label` 0 THEN HypSubst' (-1) 0)
   THEN Eq) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `polymorphic-choice-base`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  (EqTypeCD  THENA  Auto)
  THEN  RepeatFor  2  ((FunExt  THENA  Auto))
  THEN  Reduce  0
  THEN  (PointwiseFunctionalityForEquality  (-2)  THENA  Auto)
  THEN  (PointwiseFunctionalityForEquality  (-1)  THENA  Auto)
  THEN  (RWO  "2"  0  THEN  Auto)
  THEN  (Unfold  `label`  0  THEN  HypSubst'  (-1)  0)
  THEN  Eq)

---

Home Index