### Nuprl Lemma : non-pair-listunion

`∀[A,B:Type]. ∀[L:Unit ⋃ (A × B)].  L ∈ Unit supposing ispair(L) = ff`

Proof

Definitions occuring in Statement :  b-union: `A ⋃ B` bfalse: `ff` btrue: `tt` bool: `𝔹` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` ispair: `if z is a pair then a otherwise b` unit: `Unit` member: `t ∈ T` product: `x:A × B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uimplies: `b supposing a` member: `t ∈ T` b-union: `A ⋃ B` tunion: `⋃x:A.B[x]` bool: `𝔹` unit: `Unit` ifthenelse: `if b then t else f fi ` pi2: `snd(t)` not: `¬A` implies: `P `` Q` false: `False` prop: `ℙ`
Lemmas referenced :  btrue_neq_bfalse equal_wf bool_wf ispair_wf_listunion bfalse_wf b-union_wf unit_wf2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut sqequalHypSubstitution imageElimination productElimination thin unionElimination equalityElimination sqequalRule axiomEquality equalityTransitivity hypothesis equalitySymmetry lemma_by_obid independent_functionElimination voidElimination isectElimination hypothesisEquality productEquality universeEquality

Latex:
\mforall{}[A,B:Type].  \mforall{}[L:Unit  \mcup{}  (A  \mtimes{}  B)].    L  \mmember{}  Unit  supposing  ispair(L)  =  ff

Date html generated: 2016_05_15-PM-10_09_30
Last ObjectModification: 2015_12_27-PM-05_59_29

Theory : eval!all

Home Index