Nuprl Lemma : map_nil_lemma

f:Top. (map(f;[]) [])


Proof




Definitions occuring in Statement :  map: map(f;as) nil: [] top: Top all: x:A. B[x] sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T map: map(f;as) so_lambda: so_lambda(x,y,z.t[x; y; z]) top: Top so_apply: x[s1;s2;s3]
Lemmas referenced :  top_wf list_ind_nil_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut hypothesis lemma_by_obid sqequalRule sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality

Latex:
\mforall{}f:Top.  (map(f;[])  \msim{}  [])



Date html generated: 2016_05_14-AM-06_28_23
Last ObjectModification: 2015_12_26-PM-00_40_58

Theory : list_0


Home Index