Nuprl Lemma : list_ind_nil_lemma

A,x:Top.  (rec-case([]) of [] => h::t => r.A[h;t;r] x)


Definitions occuring in Statement :  list_ind: list_ind nil: [] top: Top so_apply: x[s1;s2;s3] all: x:A. B[x] sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T list_ind: list_ind nil: [] it:
Lemmas referenced :  top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut hypothesis lemma_by_obid sqequalRule callbyvalueReduce sqleReflexivity

\mforall{}A,x:Top.    (rec-case([])  of  []  =>  x  |  h::t  =>  r.A[h;t;r]  \msim{}  x)

Date html generated: 2016_05_14-AM-06_26_40
Last ObjectModification: 2015_12_26-PM-00_41_51

Theory : list_0

Home Index