### Nuprl Lemma : isaxiom_wf_listunion

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

Proof

Definitions occuring in Statement :  b-union: `A ⋃ B` bfalse: `ff` btrue: `tt` bool: `𝔹` uall: `∀[x:A]. B[x]` isaxiom: `if z = Ax 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 :  btrue_wf bfalse_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)].    (isaxiom(L)  \mmember{}  \mBbbB{})

Date html generated: 2016_05_14-AM-06_25_10
Last ObjectModification: 2015_12_26-PM-00_42_39

Theory : list_0

Home Index