Nuprl Lemma : callbyvalue-exception-type

[T:Type]. ∀[x:T]. ∀[B:Top].  eval in B[z] supposing exception-type(T)


Proof




Definitions occuring in Statement :  exception-type: exception-type(T) callbyvalue: callbyvalue uimplies: supposing a uall: [x:A]. B[x] top: Top so_apply: x[s] universe: Type sqequal: t
Definitions unfolded in proof :  uimplies: supposing a member: t ∈ T uall: [x:A]. B[x] exception-type: exception-type(T) squash: T iff: ⇐⇒ Q and: P ∧ Q implies:  Q rev_implies:  Q
Lemmas referenced :  exception-type_wf top_wf
Rules used in proof :  universeEquality equalitySymmetry equalityTransitivity because_Cache isect_memberEquality sqequalRule hypothesisEquality thin isectElimination sqequalHypSubstitution lemma_by_obid axiomSqEquality hypothesis pointwiseFunctionality cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution independent_isectElimination closedConclusion baseApply baseClosed imageMemberEquality imageElimination exceptionSqequal axiomEquality sqequalExtensionalEquality independent_pairFormation Error :lambdaFormation_alt,  Error :universeIsType,  sqequalIntensionalEquality

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].  \mforall{}[B:Top].    eval  z  =  x  in  B[z]  \msim{}  x  supposing  exception-type(T)



Date html generated: 2019_06_20-AM-11_20_56
Last ObjectModification: 2018_10_15-PM-03_31_54

Theory : call!by!value_1


Home Index