Nuprl Lemma : value-type-has-value

[T:Type]. ∀[x:T]. (x)↓ supposing value-type(T)


Proof




Definitions occuring in Statement :  value-type: value-type(T) has-value: (a)↓ uimplies: supposing a uall: [x:A]. B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a has-value: (a)↓ value-type: value-type(T) prop:
Lemmas referenced :  sqle_wf_base value-type_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution axiomSqleEquality hypothesis hypothesisEquality isect_memberEquality isectElimination thin because_Cache lemma_by_obid equalityTransitivity equalitySymmetry universeEquality pointwiseFunctionality independent_isectElimination callbyvalueReduce baseClosed

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].  (x)\mdownarrow{}  supposing  value-type(T)



Date html generated: 2016_05_13-PM-03_24_31
Last ObjectModification: 2016_01_14-PM-06_45_24

Theory : call!by!value_1


Home Index