---

Step * 1 2 1 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 ≤ ⊥
4. f Ax ≤ ⊥
⊢ f ~ λx.x
BY
{ (Fold `it` (-1) THEN (Assert f ⋅ ∈ Unit BY (Assert ⌜f ∈ Unit ⟶ Unit⌝⋅ THEN Auto))) }

1
1. f : Base
2. f ∈ ⋂T:Type. (T ⟶ T)
3. ∀[x:Base]. ∀[z:(x)↓].  if x is an integer then True else f x ≤ ⊥
4. f ⋅ ≤ ⊥
5. f ⋅ ∈ Unit
⊢ f ~ λx.x

---

Latex:

---

Latex:

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


By

---

Latex:
(Fold  `it`  (-1)  THEN  (Assert  f  \mcdot{}  \mmember{}  Unit  BY  (Assert  \mkleeneopen{}f  \mmember{}  Unit  {}\mrightarrow{}  Unit\mkleeneclose{}\mcdot{}  THEN  Auto)))

---

Home Index