Nuprl Lemma : subtype_rel_tagged+_general

[T,A,B:Type]. ∀[z:Atom].  (T ⊆|+ z:B) supposing ((T ⊆z:B) and (T ⊆A))


Definitions occuring in Statement :  tagged+: |+ z:B tag-case: z:T uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] atom: Atom universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a tagged+: |+ z:B isect2: T1 ⋂ T2 subtype_rel: A ⊆B ifthenelse: if then else fi  bool: 𝔹
Lemmas referenced :  bool_wf subtype_rel_wf tag-case_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lambdaEquality isect_memberEquality hypothesisEquality applyEquality sqequalHypSubstitution unionElimination thin hypothesis lemma_by_obid axiomEquality isectElimination because_Cache equalityTransitivity equalitySymmetry atomEquality universeEquality

\mforall{}[T,A,B:Type].  \mforall{}[z:Atom].    (T  \msubseteq{}r  A  |+  z:B)  supposing  ((T  \msubseteq{}r  z:B)  and  (T  \msubseteq{}r  A))

Date html generated: 2016_05_15-PM-06_46_30
Last ObjectModification: 2015_12_27-AM-11_49_15

Theory : general

Home Index