### Nuprl Lemma : member-co-list-islist

`∀[T:Type]. ∀[L:colist(T)].  L ∈ co-list-islist(T) supposing (is-list(L))↓`

Proof

Definitions occuring in Statement :  co-list-islist: `co-list-islist(T)` is-list: `is-list(t)` colist: `colist(T)` has-value: `(a)↓` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` member: `t ∈ T` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` bool: `𝔹` prop: `ℙ` co-list-islist: `co-list-islist(T)`
Lemmas referenced :  is-list-wf-co-list has-value_wf-partial bool_wf union-value-type unit_wf2 colist_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_isectElimination sqequalRule because_Cache dependent_set_memberEquality axiomEquality equalityTransitivity equalitySymmetry universeIsType universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[L:colist(T)].    L  \mmember{}  co-list-islist(T)  supposing  (is-list(L))\mdownarrow{}

Date html generated: 2019_10_16-AM-11_38_26
Last ObjectModification: 2018_09_26-PM-09_35_02

Theory : eval!all

Home Index