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