---

Step * 1 2 of Lemma polymorphic-id-unique-sq


1. f : Base
2. f ∈ ⋂T:Type. (T ⟶ T)
3. ⋂x:Base. ⋂z:(x)↓.  if x is an integer then True else f x ≤ ⊥
⊢ f ~ λx.x
BY
{ (Fold `uall` (-1)
   THEN (InstHyp [⌜Ax⌝;⌜Ax⌝] (-1)⋅ THENA Auto)
   THEN Reduce (-1)
   THEN Fold `it` (-1)
   THEN (Assert f ⋅ ∈ Unit BY
               (Assert ⌜f ∈ Unit ⟶ Unit⌝⋅ THEN Auto))
   THEN (Subst' f ⋅ ~ ⋅ -2 THENA Auto)
   THEN (Assert ⌜False⌝⋅ THEN Auto THEN ThinVar `f')
   THEN (Assert ⋅ ~ ⊥ BY
               (SqequalSqle THEN Auto))
   THEN ((Assert (⋅)↓ BY Auto) THEN HypSubst' (-2) (-1))
   THEN BotDiv) }

---

Latex:

---

Latex:

1.  f  :  Base
2.  f  \mmember{}  \mcap{}T:Type.  (T  {}\mrightarrow{}  T)
3.  \mcap{}x:Base.  \mcap{}z:(x)\mdownarrow{}.    if  x  is  an  integer  then  True  else  f  x  \mleq{}  \mbot{}
\mvdash{}  f  \msim{}  \mlambda{}x.x


By

---

Latex:
(Fold  `uall`  (-1)
  THEN  (InstHyp  [\mkleeneopen{}Ax\mkleeneclose{};\mkleeneopen{}Ax\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  Fold  `it`  (-1)
  THEN  (Assert  f  \mcdot{}  \mmember{}  Unit  BY
                          (Assert  \mkleeneopen{}f  \mmember{}  Unit  {}\mrightarrow{}  Unit\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (Subst'  f  \mcdot{}  \msim{}  \mcdot{}  -2  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  ThinVar  `f')
  THEN  (Assert  \mcdot{}  \msim{}  \mbot{}  BY
                          (SqequalSqle  THEN  Auto))
  THEN  ((Assert  (\mcdot{})\mdownarrow{}  BY  Auto)  THEN  HypSubst'  (-2)  (-1))
  THEN  BotDiv)

---

Home Index