Nuprl Lemma : atom1-valueall-type

valueall-type(Atom1)


Proof




Definitions occuring in Statement :  valueall-type: valueall-type(T) atom: Atom$n
Definitions unfolded in proof :  valueall-type: valueall-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)↓ squash: T
Lemmas referenced :  sq_stable__has-value evalall-atom1 base_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin sqequalRule baseApply closedConclusion baseClosed hypothesisEquality hypothesis independent_functionElimination equalityTransitivity equalitySymmetry Error :inhabitedIsType,  Error :lambdaFormation_alt,  callbyvalueAtom1 because_Cache Error :equalityIsType1,  dependent_functionElimination imageMemberEquality imageElimination Error :equalityIsType4,  Error :universeIsType,  atomnEquality

Latex:
valueall-type(Atom1)



Date html generated: 2019_06_20-AM-11_21_17
Last ObjectModification: 2018_10_15-PM-04_55_38

Theory : call!by!value_1


Home Index