---

Step * of Lemma polymorphic-id-unique-sq

∀f:⋂T:Type. (T ⟶ T). (f ~ λx.x)
BY
{ Assert ⌜∀f:Base. ((f ∈ ⋂T:Type. (T ⟶ T)) ⇒ (f ~ λx.x))⌝⋅ }

1
.....assertion..... 
∀f:Base. ((f ∈ ⋂T:Type. (T ⟶ T)) ⇒ (f ~ λx.x))

2
1. ∀f:Base. ((f ∈ ⋂T:Type. (T ⟶ T)) ⇒ (f ~ λx.x))
⊢ ∀f:⋂T:Type. (T ⟶ T). (f ~ λx.x)

---

Latex:

---

Latex:
\mforall{}f:\mcap{}T:Type.  (T  {}\mrightarrow{}  T).  (f  \msim{}  \mlambda{}x.x)


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}f:Base.  ((f  \mmember{}  \mcap{}T:Type.  (T  {}\mrightarrow{}  T))  {}\mRightarrow{}  (f  \msim{}  \mlambda{}x.x))\mkleeneclose{}\mcdot{}

---

Home Index