Nuprl Lemma : type-value-type

value-type(Type)


Proof




Definitions occuring in Statement :  value-type: value-type(T) universe: Type
Definitions unfolded in proof :  value-type: value-type(T) uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T sq_stable: SqStable(P) implies:  Q all: x:A. B[x] has-value: (a)↓ prop: squash: T
Lemmas referenced :  sq_stable__has-value equal_wf equal-wf-base base_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_functionElimination equalityTransitivity equalitySymmetry universeEquality lambdaFormation callbyvalueType because_Cache instantiate dependent_functionElimination sqequalRule imageMemberEquality baseClosed imageElimination

Latex:
value-type(Type)



Date html generated: 2019_06_20-AM-11_21_25
Last ObjectModification: 2018_08_01-PM-03_15_46

Theory : call!by!value_1


Home Index