Nuprl Lemma : valueall-type-value-type

[A:Type]. value-type(A) supposing valueall-type(A)


Proof




Definitions occuring in Statement :  valueall-type: valueall-type(T) value-type: value-type(T) 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 value-type: value-type(T) sq_stable: SqStable(P) implies:  Q all: x:A. B[x] has-value: (a)↓ has-valueall: has-valueall(a) prop: squash: T
Lemmas referenced :  sq_stable__has-value evalall-reduce valueall-type-has-valueall equal_wf equal-wf-base base_wf valueall-type_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_functionElimination equalityTransitivity equalitySymmetry lambdaFormation because_Cache independent_isectElimination dependent_functionElimination sqequalRule imageMemberEquality baseClosed imageElimination isect_memberEquality axiomSqleEquality cumulativity universeEquality

Latex:
\mforall{}[A:Type].  value-type(A)  supposing  valueall-type(A)



Date html generated: 2017_04_14-AM-07_35_13
Last ObjectModification: 2017_02_27-PM-03_07_58

Theory : fun_1


Home Index