### Nuprl Lemma : length_one

`∀[T:Type]. ∀L:T List. uiff(||L|| = 1 ∈ ℤ;∃x:T. (L = [x] ∈ (T List)))`

Proof

Definitions occuring in Statement :  length: `||as||` cons: `[a / b]` nil: `[]` list: `T List` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` natural_number: `\$n` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` member: `t ∈ T` or: `P ∨ Q` sq_type: `SQType(T)` implies: `P `` Q` guard: `{T}` true: `True` false: `False` cons: `[a / b]` top: `Top` exists: `∃x:A. B[x]` prop: `ℙ` subtype_rel: `A ⊆r B` nat: `ℕ` squash: `↓T` subtract: `n - m` sq_stable: `SqStable(P)` le: `A ≤ B` not: `¬A` less_than': `less_than'(a;b)` so_lambda: `λ2x.t[x]` so_apply: `x[s]` ge: `i ≥ j `
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation independent_pairFormation cut introduction axiomEquality hypothesis thin rename hypothesisEquality extract_by_obid sqequalHypSubstitution isectElimination dependent_functionElimination unionElimination sqequalRule instantiate cumulativity intEquality independent_isectElimination equalityTransitivity equalitySymmetry independent_functionElimination natural_numberEquality voidElimination promote_hyp hypothesis_subsumption productElimination isect_memberEquality voidEquality dependent_pairFormation because_Cache sqequalIntensionalEquality applyEquality applyLambdaEquality setElimination imageMemberEquality baseClosed addEquality lambdaEquality minusEquality imageElimination dependent_set_memberEquality hyp_replacement universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  uiff(||L||  =  1;\mexists{}x:T.  (L  =  [x]))

Date html generated: 2017_04_14-AM-08_35_38
Last ObjectModification: 2017_02_27-PM-03_28_05

Theory : list_0

Home Index