---

Step * of Lemma subtype_pos_polymorphism_test

((⋂T:Type. (ℙ ⟶ ℤ ⟶ (T × T + T))) ⊆r (ℙ ⟶ ℤ ⟶ (Void × Void + Void)))
∧ ((ℙ ⟶ ℤ ⟶ (Void × Void + Void)) ⊆r (⋂T:Type. (ℙ ⟶ ℤ ⟶ (T × T + T))))
BY
{ RepeatFor 3 ((D 0 THEN Auto)) }

---

Latex:

---

Latex:
((\mcap{}T:Type.  (\mBbbP{}  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  (T  \mtimes{}  T  +  T)))  \msubseteq{}r  (\mBbbP{}  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  (Void  \mtimes{}  Void  +  Void)))
\mwedge{}  ((\mBbbP{}  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  (Void  \mtimes{}  Void  +  Void))  \msubseteq{}r  (\mcap{}T:Type.  (\mBbbP{}  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  (T  \mtimes{}  T  +  T))))


By

---

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

---

Home Index