Nuprl Lemma : csm-aux_wf

[V:Type]. ∀[sm:CSM(V)]. ∀[i:V].  (csm-aux(sm;i) ∈ Type)


Proof




Definitions occuring in Statement :  csm-aux: csm-aux(sm;i) csm: CSM(V) uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T csm: CSM(V) csm-aux: csm-aux(sm;i) pi2: snd(t) pi1: fst(t)
Lemmas referenced :  csm_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin sqequalRule applyEquality hypothesisEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality isectElimination because_Cache lemma_by_obid universeEquality

Latex:
\mforall{}[V:Type].  \mforall{}[sm:CSM(V)].  \mforall{}[i:V].    (csm-aux(sm;i)  \mmember{}  Type)



Date html generated: 2016_05_15-PM-05_10_56
Last ObjectModification: 2015_12_27-PM-02_23_22

Theory : general


Home Index