Nuprl Lemma : has-value-extensionality

`∀[a,b:Base].  (a)↓ = (b)↓ ∈ ℙ supposing (a)↓ `⇐⇒` (b)↓`

Proof

Definitions occuring in Statement :  has-value: `(a)↓` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` prop: `ℙ` iff: `P `⇐⇒` Q` base: `Base` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` iff: `P `⇐⇒` Q` and: `P ∧ Q` has-value: `(a)↓` prop: `ℙ` implies: `P `` Q` rev_implies: `P `` Q` squash: `↓T`
Lemmas referenced :  has-value_wf_base istype-base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalHypSubstitution productElimination thin sqleExtensionalEquality independent_pairFormation Error :lambdaFormation_alt,  independent_functionElimination hypothesis Error :universeIsType,  extract_by_obid isectElimination hypothesisEquality sqequalRule imageMemberEquality baseClosed Error :productIsType,  Error :functionIsType,  because_Cache Error :isect_memberEquality_alt,  axiomEquality Error :isectIsTypeImplies,  Error :inhabitedIsType

Latex:
\mforall{}[a,b:Base].    (a)\mdownarrow{}  =  (b)\mdownarrow{}  supposing  (a)\mdownarrow{}  \mLeftarrow{}{}\mRightarrow{}  (b)\mdownarrow{}

Date html generated: 2019_06_20-AM-11_20_34
Last ObjectModification: 2018_10_16-PM-01_47_32

Theory : call!by!value_1

Home Index