Nuprl Lemma : atom-valueall-type

valueall-type(Atom)


Proof




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

Latex:
valueall-type(Atom)



Date html generated: 2019_06_20-AM-11_21_13
Last ObjectModification: 2018_10_15-AM-08_52_52

Theory : call!by!value_1


Home Index