Nuprl Lemma : mobj-data_wf

[s:MutualRectypeSpec]. ∀[x:mobj(s)].  (mobj-data(x) ∈ mtype(s;mobj-kind(x)))


Proof




Definitions occuring in Statement :  mobj-data: mobj-data(x) mobj-kind: mobj-kind(x) mobj: mobj(L) mtype: mtype(L;i) mrec_spec: MutualRectypeSpec uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T mobj-data: mobj-data(x) mobj: mobj(L) pi2: snd(t) mobj-kind: mobj-kind(x) pi1: fst(t)
Lemmas referenced :  mobj_wf mrec_spec_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule sqequalHypSubstitution productElimination thin hypothesisEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry Error :universeIsType,  extract_by_obid isectElimination Error :isect_memberEquality_alt,  Error :isectIsTypeImplies,  Error :inhabitedIsType

Latex:
\mforall{}[s:MutualRectypeSpec].  \mforall{}[x:mobj(s)].    (mobj-data(x)  \mmember{}  mtype(s;mobj-kind(x)))



Date html generated: 2019_06_20-PM-02_15_21
Last ObjectModification: 2019_02_28-PM-02_37_06

Theory : tuples


Home Index