Nuprl Lemma : seq-comp-item

[T:Type]. ∀[s:sequence(T)]. ∀[f,i:Top].  (f s[i] s[i])


Proof




Definitions occuring in Statement :  seq-comp: s seq-item: s[i] sequence: sequence(T) uall: [x:A]. B[x] top: Top apply: a universe: Type sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T sequence: sequence(T) seq-item: s[i] seq-comp: s pi2: snd(t)
Lemmas referenced :  top_wf sequence_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin sqequalRule hypothesis sqequalAxiom extract_by_obid isect_memberEquality isectElimination hypothesisEquality because_Cache universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[s:sequence(T)].  \mforall{}[f,i:Top].    (f  o  s[i]  \msim{}  f  s[i])



Date html generated: 2018_07_25-PM-01_28_28
Last ObjectModification: 2018_06_11-PM-04_24_58

Theory : arithmetic


Home Index