Nuprl Lemma : void-valueall-type

valueall-type(Void)


Proof




Definitions occuring in Statement :  valueall-type: valueall-type(T) void: Void
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] prop: squash: T
Lemmas referenced :  sq_stable__has-value equal_wf equal-wf-base base_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin sqequalRule baseApply closedConclusion baseClosed hypothesisEquality hypothesis independent_functionElimination equalityTransitivity equalitySymmetry voidEquality lambdaFormation voidElimination dependent_functionElimination imageMemberEquality imageElimination because_Cache

Latex:
valueall-type(Void)



Date html generated: 2017_04_14-AM-07_14_48
Last ObjectModification: 2017_02_27-PM-02_50_21

Theory : call!by!value_1


Home Index