Nuprl Lemma : sq_stable__has-value

[a:Base]. SqStable((a)↓)


Proof




Definitions occuring in Statement :  has-value: (a)↓ sq_stable: SqStable(P) uall: [x:A]. B[x] base: Base
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T sq_stable: SqStable(P) implies:  Q squash: T has-value: (a)↓ prop:
Lemmas referenced :  squash_wf has-value_wf_base base_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation sqequalHypSubstitution imageElimination hypothesis axiomSqleEquality lemma_by_obid isectElimination thin hypothesisEquality sqequalRule lambdaEquality dependent_functionElimination

Latex:
\mforall{}[a:Base].  SqStable((a)\mdownarrow{})



Date html generated: 2016_05_13-PM-03_25_15
Last ObjectModification: 2015_12_26-AM-09_29_26

Theory : call!by!value_1


Home Index