### Nuprl Lemma : evalall-reduce

`∀[T:Type]. ∀[t:T].  evalall(t) ~ t supposing valueall-type(T)`

Proof

Definitions occuring in Statement :  valueall-type: `valueall-type(T)` evalall: `evalall(t)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` universe: `Type` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` valueall-type: `valueall-type(T)` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` rev_implies: `P `` Q` squash: `↓T`
Lemmas referenced :  evalall-sqequal valueall-type_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalHypSubstitution pointwiseFunctionality extract_by_obid isectElimination thin hypothesisEquality independent_isectElimination hypothesis equalityTransitivity equalitySymmetry because_Cache sqequalRule sqequalExtensionalEquality independent_pairFormation Error :lambdaFormation_alt,  Error :universeIsType,  sqequalIntensionalEquality imageMemberEquality baseClosed axiomSqEquality Error :isect_memberEquality_alt,  Error :isectIsTypeImplies,  Error :inhabitedIsType,  universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[t:T].    evalall(t)  \msim{}  t  supposing  valueall-type(T)

Date html generated: 2019_06_20-PM-00_26_50
Last ObjectModification: 2018_10_15-PM-00_48_54

Theory : fun_1

Home Index