Nuprl Lemma : l_sum_nil_lemma

l_sum([]) 0


Proof




Definitions occuring in Statement :  l_sum: l_sum(L) nil: [] natural_number: $n sqequal: t
Definitions unfolded in proof :  l_sum: l_sum(L) all: x:A. B[x] member: t ∈ T top: Top
Lemmas referenced :  reduce_nil_lemma
Rules used in proof :  sqequalSubstitution sqequalRule sqequalTransitivity computationStep sqequalReflexivity cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality hypothesis

Latex:
l\_sum([])  \msim{}  0



Date html generated: 2016_05_14-PM-02_52_22
Last ObjectModification: 2015_12_26-PM-02_34_40

Theory : list_1


Home Index