### Nuprl Lemma : atom-implies-ispair-right

`∀[b,c:Top]. ∀[a:Atom].  (if a is a pair then b otherwise c ~ c)`

Proof

Definitions occuring in Statement :  uall: `∀[x:A]. B[x]` top: `Top` ispair: `if z is a pair then a otherwise b` atom: `Atom` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` subtype_rel: `A ⊆r B` implies: `P `` Q` uimplies: `b supposing a` or: `P ∨ Q` not: `¬A` false: `False`
Lemmas referenced :  has-value-implies-dec-ispair atom_subtype_base value-type-has-value atom-value-type not-btrue-sqeq-bfalse top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule thin lemma_by_obid sqequalHypSubstitution dependent_functionElimination hypothesisEquality applyEquality hypothesis independent_functionElimination isectElimination atomEquality independent_isectElimination unionElimination isatomReduceTrue voidElimination sqequalAxiom isect_memberEquality because_Cache

Latex:
\mforall{}[b,c:Top].  \mforall{}[a:Atom].    (if  a  is  a  pair  then  b  otherwise  c  \msim{}  c)

Date html generated: 2016_05_13-PM-03_28_16
Last ObjectModification: 2015_12_26-AM-09_27_26

Theory : call!by!value_1

Home Index