Nuprl Lemma : seq-tl-item
∀[T:Type]. ∀[s:sequence(T)]. ∀[i:Top]. (seq-tl(s)[i] ~ s[i + 1])
Proof
Definitions occuring in Statement :
seq-tl: seq-tl(s),
seq-item: s[i],
sequence: sequence(T),
uall: ∀[x:A]. B[x],
top: Top,
add: n + m,
natural_number: $n,
universe: Type,
sqequal: s ~ t
Definitions unfolded in proof :
pi2: snd(t),
seq-tl: seq-tl(s),
seq-item: s[i],
sequence: sequence(T),
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
sequence_wf,
top_wf
Rules used in proof :
universeEquality,
hypothesisEquality,
isectElimination,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
productElimination,
sqequalHypSubstitution,
sqequalAxiom,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[T:Type]. \mforall{}[s:sequence(T)]. \mforall{}[i:Top]. (seq-tl(s)[i] \msim{} s[i + 1])
Date html generated:
2018_07_25-PM-01_29_18
Last ObjectModification:
2018_06_17-PM-10_13_27
Theory : arithmetic
Home
Index