Nuprl Lemma : subtype_pos_polymorphism_test

((⋂T:Type. (ℙ ⟶ ℤ ⟶ (T × T))) ⊆(ℙ ⟶ ℤ ⟶ (Void × Void Void)))
∧ ((ℙ ⟶ ℤ ⟶ (Void × Void Void)) ⊆(⋂T:Type. (ℙ ⟶ ℤ ⟶ (T × T))))


Proof




Definitions occuring in Statement :  subtype_rel: A ⊆B prop: and: P ∧ Q isect: x:A. B[x] function: x:A ⟶ B[x] product: x:A × B[x] union: left right int: void: Void universe: Type
Definitions unfolded in proof :  and: P ∧ Q subtype_rel: A ⊆B member: t ∈ T prop: uall: [x:A]. B[x] so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a all: x:A. B[x]
Lemmas referenced :  subtype_rel_dep_function subtype_rel_union subtype_rel_product
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity independent_pairFormation lambdaEquality isectElimination voidEquality equalityTransitivity equalitySymmetry hypothesis isectEquality universeEquality functionEquality cumulativity intEquality unionEquality productEquality hypothesisEquality thin isect_memberEquality cut applyEquality instantiate lemma_by_obid sqequalHypSubstitution sqequalRule because_Cache independent_isectElimination lambdaFormation voidElimination

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))))



Date html generated: 2016_05_15-PM-07_49_13
Last ObjectModification: 2015_12_27-AM-11_07_20

Theory : general


Home Index