Nuprl Lemma : Id-has-valueall

[x:Id]. has-valueall(x)


Proof




Definitions occuring in Statement :  Id: Id has-valueall: has-valueall(a) uall: [x:A]. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a has-valueall: has-valueall(a) has-value: (a)↓
Lemmas referenced :  valueall-type-has-valueall Id_wf Id-valueall-type
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis independent_isectElimination hypothesisEquality sqequalRule axiomSqleEquality

Latex:
\mforall{}[x:Id].  has-valueall(x)



Date html generated: 2016_05_14-PM-03_36_44
Last ObjectModification: 2015_12_26-PM-05_59_16

Theory : decidable!equality


Home Index