### Nuprl Lemma : co-list-cases

`∀[T:Type]`
`  ∀x:colist(T)`
`    (((↑isaxiom(x)) ∧ (x = Ax ∈ Unit)) ∨ ((↑ispair(x)) ∧ (∃t:T. ∃y:colist(T). (x = <t, y> ∈ (T × colist(T))))))`

Proof

Definitions occuring in Statement :  colist: `colist(T)` assert: `↑b` bfalse: `ff` btrue: `tt` uall: `∀[x:A]. B[x]` ispair: `if z is a pair then a otherwise b` isaxiom: `if z = Ax then a otherwise b` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` or: `P ∨ Q` and: `P ∧ Q` unit: `Unit` pair: `<a, b>` product: `x:A × B[x]` universe: `Type` equal: `s = t ∈ T` axiom: `Ax`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` subtype_rel: `A ⊆r B` implies: `P `` Q` b-union: `A ⋃ B` tunion: `⋃x:A.B[x]` bool: `𝔹` unit: `Unit` ifthenelse: `if b then t else f fi ` pi2: `snd(t)` assert: `↑b` btrue: `tt` bfalse: `ff` or: `P ∨ Q` and: `P ∧ Q` true: `True` prop: `ℙ` false: `False` exists: `∃x:A. B[x]` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  co-list-subtype b-union_wf unit_wf2 colist_wf false_wf equal_wf exists_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut hypothesisEquality applyEquality introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis sqequalRule productEquality cumulativity imageElimination productElimination unionElimination equalityElimination inlEquality independent_pairEquality axiomEquality equalityTransitivity equalitySymmetry voidElimination dependent_functionElimination independent_functionElimination inrEquality natural_numberEquality dependent_pairEquality because_Cache lambdaEquality universeEquality

Latex:
\mforall{}[T:Type]
\mforall{}x:colist(T).  (((\muparrow{}isaxiom(x))  \mwedge{}  (x  =  Ax))  \mvee{}  ((\muparrow{}ispair(x))  \mwedge{}  (\mexists{}t:T.  \mexists{}y:colist(T).  (x  =  <t,  y>))))

Date html generated: 2018_05_21-PM-10_19_44
Last ObjectModification: 2017_07_26-PM-06_37_09

Theory : eval!all

Home Index