### Nuprl Lemma : co-list-cases2

`∀[T:Type]. ∀x:colist(T). ((x = Ax ∈ colist(T)) ∨ (∃t:T. ∃y:colist(T). (x = <t, y> ∈ colist(T))))`

Proof

Definitions occuring in Statement :  colist: `colist(T)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` or: `P ∨ Q` pair: `<a, b>` 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` ext-eq: `A ≡ B` and: `P ∧ Q` 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)` or: `P ∨ Q` it: `⋅` guard: `{T}` uimplies: `b supposing a` exists: `∃x:A. B[x]` respects-equality: `respects-equality(S;T)`
Lemmas referenced :  colist-ext subtype_rel_b-union-right unit_wf2 colist_wf it_wf subtype_rel_b-union-left unit_subtype_colist subtype_rel_transitivity b-union_wf co-list-subtype subtype-respects-equality product_subtype_colist istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality productElimination lambdaEquality_alt applyEquality hypothesis productEquality sqequalRule productIsType universeIsType because_Cache inhabitedIsType imageElimination unionElimination equalityElimination inlEquality_alt axiomEquality independent_isectElimination equalityIstype baseClosed independent_pairEquality sqequalBase equalitySymmetry dependent_functionElimination independent_functionElimination inrEquality_alt dependent_pairEquality_alt equalityTransitivity instantiate universeEquality

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

Date html generated: 2020_05_20-AM-09_07_47
Last ObjectModification: 2019_12_31-PM-07_06_24

Theory : eval!all

Home Index