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: supposing a guard: {T} lelt: i ≤ j < k int_seg: {i..j-} prop: implies:  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