### Nuprl Lemma : axiom-listunion

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

Proof

Definitions occuring in Statement :  b-union: `A ⋃ B` bfalse: `ff` btrue: `tt` bool: `𝔹` uimplies: `b supposing a` 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` 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`
Lemmas referenced :  bool_wf btrue_wf bfalse_wf b-union_wf unit_wf2 btrue_neq_bfalse
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  cut sqequalHypSubstitution imageElimination productElimination thin unionElimination equalityElimination sqequalRule hypothesisEquality hypothesis Error :equalityIsType3,  Error :universeIsType,  introduction extract_by_obid baseClosed isectElimination productEquality Error :inhabitedIsType,  universeEquality equalitySymmetry independent_functionElimination voidElimination

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

Date html generated: 2019_06_20-PM-00_38_05
Last ObjectModification: 2018_10_06-AM-11_20_39

Theory : list_0

Home Index