Nuprl Lemma : polymorphic-choice-base-sq

f:Base. ((f ∈ ⋂A:Type. (A ⟶ A ⟶ A))  ((f ~ λx.if is lambda then λy.x otherwise ⊥) ∨ (f ~ λx,y. y)))


Proof




Definitions occuring in Statement :  bottom: islambda: if is lambda then otherwise b all: x:A. B[x] implies:  Q or: P ∨ Q member: t ∈ T apply: a lambda: λx.A[x] isect: x:A. B[x] function: x:A ⟶ B[x] base: Base universe: Type sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T or: P ∨ Q guard: {T} uall: [x:A]. B[x] prop:
Lemmas referenced :  polymorphic-choice-base equal-wf-base base_wf poly-choice-eta-2 poly-choice-eta-1
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin equalityTransitivity hypothesis equalitySymmetry unionElimination inlFormation sqequalIntensionalEquality hypothesisEquality baseClosed sqequalRule inrFormation baseApply closedConclusion instantiate isectElimination isectEquality universeEquality cumulativity functionEquality because_Cache independent_functionElimination

Latex:
\mforall{}f:Base
    ((f  \mmember{}  \mcap{}A:Type.  (A  {}\mrightarrow{}  A  {}\mrightarrow{}  A))  {}\mRightarrow{}  ((f  \msim{}  \mlambda{}x.if  f  x  is  lambda  then  \mlambda{}y.x  otherwise  \mbot{})  \mvee{}  (f  \msim{}  \mlambda{}x,y.  y))\000C)



Date html generated: 2018_05_21-PM-01_16_12
Last ObjectModification: 2018_05_01-PM-04_37_58

Theory : num_thy_1


Home Index