---

Step * 2 1 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
BY
{ TACTIC:(UseWitness ⌜Ax⌝⋅ 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


By

---

Latex:
TACTIC:(UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index