Nuprl Lemma : not-ispair

[t,a,b:Base].
  ∀[x,y:Top].  (if is pair then otherwise y) supposing if is pair then inl otherwise inr b  inr 


Proof




Definitions occuring in Statement :  uimplies: supposing a uall: [x:A]. B[x] top: Top ispair: if is pair then otherwise b inr: inr  inl: inl x base: Base sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a has-value: (a)↓ implies:  Q false: False sq_type: SQType(T) all: x:A. B[x] guard: {T} top: Top
Lemmas referenced :  base_wf top_wf not_zero_sqequal_one subtype_rel_self subtype_base_sq is-exception_wf has-value_wf_base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule thin hypothesis divergentSqle sqleReflexivity lemma_by_obid sqequalHypSubstitution isectElimination baseClosed callbyvalueIspair ispairCases because_Cache hypothesisEquality instantiate independent_isectElimination independent_functionElimination voidElimination promote_hyp dependent_functionElimination sqequalAxiom isect_memberEquality voidEquality sqequalIntensionalEquality baseApply closedConclusion equalityTransitivity equalitySymmetry

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



Date html generated: 2016_05_13-PM-03_22_01
Last ObjectModification: 2016_01_14-PM-06_47_11

Theory : call!by!value_1


Home Index