### Nuprl Lemma : ispair_wf_listunion

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

Proof

Definitions occuring in Statement :  b-union: `A ⋃ B` bfalse: `ff` btrue: `tt` bool: `𝔹` 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`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` 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)`
Lemmas referenced :  bfalse_wf btrue_wf b-union_wf unit_wf2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution imageElimination productElimination thin unionElimination equalityElimination sqequalRule lemma_by_obid hypothesis axiomEquality equalityTransitivity equalitySymmetry isectElimination productEquality hypothesisEquality isect_memberEquality because_Cache universeEquality

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

Date html generated: 2016_05_15-PM-10_09_26
Last ObjectModification: 2015_12_27-PM-05_59_34

Theory : eval!all

Home Index