### Nuprl Lemma : colength-positive2

`∀[T:Type]. ∀[L:T List].`
`  ∀n:ℕ`
`    (0 < n`
`    `` (colength(L) = n ∈ ℤ)`
`    `` {(fst(L) ∈ T) ∧ (snd(L) ∈ T List) ∧ (colength(L) = (1 + colength(snd(L))) ∈ ℤ) ∧ (L ~ [fst(L) / (snd(L))])})`

Proof

Definitions occuring in Statement :  cons: `[a / b]` list: `T List` colength: `colength(L)` nat: `ℕ` less_than: `a < b` uall: `∀[x:A]. B[x]` guard: `{T}` pi1: `fst(t)` pi2: `snd(t)` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` member: `t ∈ T` add: `n + m` natural_number: `\$n` int: `ℤ` universe: `Type` sqequal: `s ~ t` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` implies: `P `` Q` guard: `{T}` nat: `ℕ` subtype_rel: `A ⊆r B` uimplies: `b supposing a` and: `P ∧ Q` prop: `ℙ`
Lemmas referenced :  colength-positive less_than_transitivity1 colength_wf_list le_weakening equal_wf nat_wf less_than_wf list_wf
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaFormation introduction independent_functionElimination equalitySymmetry natural_numberEquality setElimination rename applyEquality because_Cache sqequalRule independent_isectElimination dependent_functionElimination productElimination independent_pairEquality axiomEquality equalityTransitivity sqequalAxiom intEquality lambdaEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].
\mforall{}n:\mBbbN{}
(0  <  n
{}\mRightarrow{}  (colength(L)  =  n)
{}\mRightarrow{}  \{(fst(L)  \mmember{}  T)
\mwedge{}  (snd(L)  \mmember{}  T  List)
\mwedge{}  (colength(L)  =  (1  +  colength(snd(L))))
\mwedge{}  (L  \msim{}  [fst(L)  /  (snd(L))])\})

Date html generated: 2016_05_14-AM-06_26_17
Last ObjectModification: 2015_12_26-PM-00_42_03

Theory : list_0

Home Index