---

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


1. ∀f:Base. ((f ∈ ⋂T:Type. (T ⟶ T)) ⇒ (f ~ λx.x))
2. a : Base
3. b : Base
4. c : a = b ∈ (⋂T:Type. (T ⟶ T))
⊢ (a ~ λx.x) = (b ~ λx.x) ∈ Type
BY
{ (Refine `sqequalExtensionalEquality` [] THEN D 0 THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}f:Base.  ((f  \mmember{}  \mcap{}T:Type.  (T  {}\mrightarrow{}  T))  {}\mRightarrow{}  (f  \msim{}  \mlambda{}x.x))
2.  a  :  Base
3.  b  :  Base
4.  c  :  a  =  b
\mvdash{}  (a  \msim{}  \mlambda{}x.x)  =  (b  \msim{}  \mlambda{}x.x)


By

---

Latex:
(Refine  `sqequalExtensionalEquality`  []  THEN  D  0  THEN  Auto)

---

Home Index