---

Step * of Lemma subtype_neg_polymorphism_test

((⋂T:Type. (T ⟶ T ⟶ ℙ)) ⊆r (Top ⟶ Top ⟶ ℙ)) ∧ ((Top ⟶ Top ⟶ ℙ) ⊆r (⋂T:Type. (T ⟶ T ⟶ ℙ)))
BY
{ RepeatFor 2 ((D 0 THEN Auto)) }

---

Latex:

---

Latex:
((\mcap{}T:Type.  (T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}))  \msubseteq{}r  (Top  {}\mrightarrow{}  Top  {}\mrightarrow{}  \mBbbP{}))  \mwedge{}  ((Top  {}\mrightarrow{}  Top  {}\mrightarrow{}  \mBbbP{})  \msubseteq{}r  (\mcap{}T:Type.  (T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{})))


By

---

Latex:
RepeatFor  2  ((D  0  THEN  Auto))

---

Home Index