### Nuprl Lemma : seq-nil_wf

`∀[T:Type]. (seq-nil() ∈ sequence(T))`

Proof

Definitions occuring in Statement :  seq-nil: `seq-nil()` sequence: `sequence(T)` uall: `∀[x:A]. B[x]` member: `t ∈ T` universe: `Type`
Definitions unfolded in proof :  uimplies: `b supposing a` guard: `{T}` lelt: `i ≤ j < k` int_seg: `{i..j-}` prop: `ℙ` implies: `P `` Q` not: `¬A` false: `False` less_than': `less_than'(a;b)` and: `P ∧ Q` le: `A ≤ B` nat: `ℕ` sequence: `sequence(T)` seq-nil: `seq-nil()` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Lemmas referenced :  int_seg_wf less_than_irreflexivity less_than_transitivity1 le_wf false_wf
Rules used in proof :  universeEquality equalitySymmetry equalityTransitivity axiomEquality functionEquality voidElimination independent_functionElimination independent_isectElimination productElimination rename setElimination functionExtensionality hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid hypothesis lambdaFormation independent_pairFormation natural_numberEquality dependent_set_memberEquality dependent_pairEquality sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[T:Type].  (seq-nil()  \mmember{}  sequence(T))

Date html generated: 2018_07_25-PM-01_29_24
Last ObjectModification: 2018_06_18-PM-01_58_51

Theory : arithmetic

Home Index