### Nuprl Lemma : subtype_rel_tagged+_general

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

Proof

Definitions occuring in Statement :  tagged+: `T |+ z:B` tag-case: `z:T` uimplies: `b supposing a` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` atom: `Atom` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` tagged+: `T |+ z:B` isect2: `T1 ⋂ T2` subtype_rel: `A ⊆r B` ifthenelse: `if b then t else f 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

Latex:
\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