### Nuprl Lemma : length-in-prop-if-co-list

`∀[T:Type]. ∀[t:colist(T)].  (∃n:ℕ. (||t|| = n ∈ partial(ℤ)) ∈ ℙ)`

Proof

Definitions occuring in Statement :  length: `||as||` colist: `colist(T)` partial: `partial(T)` nat: `ℕ` uall: `∀[x:A]. B[x]` prop: `ℙ` exists: `∃x:A. B[x]` member: `t ∈ T` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` nat: `ℕ` so_apply: `x[s]` uimplies: `b supposing a`
Lemmas referenced :  exists_wf nat_wf equal_wf partial_wf length-in-bar-int-if-co-list subtype_rel_set le_wf istype-int inclusion-partial int-value-type colist_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis sqequalRule lambdaEquality_alt intEquality hypothesisEquality applyEquality because_Cache natural_numberEquality independent_isectElimination universeIsType universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[t:colist(T)].    (\mexists{}n:\mBbbN{}.  (||t||  =  n)  \mmember{}  \mBbbP{})

Date html generated: 2019_10_16-AM-11_38_19
Last ObjectModification: 2018_10_11-PM-03_19_39

Theory : eval!all

Home Index