### Nuprl Lemma : ispair-pair

`∀[t,x,y:Base].  t ∈ Top × Top supposing if t is a pair then inl x otherwise inr y  ~ inl x`

Proof

Definitions occuring in Statement :  uimplies: `b supposing a` uall: `∀[x:A]. B[x]` top: `Top` ispair: `if z is a pair then a otherwise b` member: `t ∈ T` product: `x:A × B[x]` inr: `inr x ` inl: `inl x` base: `Base` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` has-value: `(a)↓` implies: `P `` Q` top: `Top` false: `False`
Lemmas referenced :  not_zero_sqequal_one base_wf top_wf is-exception_wf has-value_wf_base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesis sqequalRule divergentSqle sqleReflexivity lemma_by_obid sqequalHypSubstitution isectElimination thin baseClosed callbyvalueIspair ispairCases hypothesisEquality lambdaFormation independent_pairEquality isect_memberEquality voidElimination voidEquality sqequalIntensionalEquality baseApply closedConclusion sqequalAxiom because_Cache independent_functionElimination equalityTransitivity equalitySymmetry axiomEquality addLevel levelHypothesis promote_hyp

Latex:
\mforall{}[t,x,y:Base].    t  \mmember{}  Top  \mtimes{}  Top  supposing  if  t  is  a  pair  then  inl  x  otherwise  inr  y    \msim{}  inl  x

Date html generated: 2016_05_13-PM-03_22_00
Last ObjectModification: 2016_01_14-PM-06_47_20

Theory : call!by!value_1

Home Index