### Nuprl Lemma : subtype_rel_record+_easy

`∀[T1,T2:𝕌']. ∀[B:T2 ⟶ 𝕌'].  ∀[z:Atom]. (T1; z:B[self] ⊆r T2; z:B[self]) supposing T1 ⊆r T2`

Proof

Definitions occuring in Statement :  record+: record+ uimplies: `b supposing a` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` so_apply: `x[s]` function: `x:A ⟶ B[x]` atom: `Atom` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` so_lambda: `λ2x.t[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B` all: `∀x:A. B[x]`
Lemmas referenced :  subtype_rel_record+ subtype_rel_self subtype_rel_wf
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality introduction sqequalRule lambdaEquality applyEquality because_Cache independent_isectElimination lambdaFormation instantiate axiomEquality atomEquality isect_memberEquality equalityTransitivity equalitySymmetry functionEquality cumulativity universeEquality

Latex:
\mforall{}[T1,T2:\mBbbU{}'].  \mforall{}[B:T2  {}\mrightarrow{}  \mBbbU{}'].    \mforall{}[z:Atom].  (T1;  z:B[self]  \msubseteq{}r  T2;  z:B[self])  supposing  T1  \msubseteq{}r  T2

Date html generated: 2016_05_15-PM-06_39_32
Last ObjectModification: 2015_12_27-AM-11_53_03

Theory : general

Home Index