Nuprl Lemma : mapcons_cons_lemma

t,h,f:Top.  (mapcons(f;[h t]) [f mapcons(f;t)])


Proof




Definitions occuring in Statement :  mapcons: mapcons(f;as) cons: [a b] top: Top all: x:A. B[x] apply: a sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T mapcons: mapcons(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_cons_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{}t,h,f:Top.    (mapcons(f;[h  /  t])  \msim{}  [f  h  t  /  mapcons(f;t)])



Date html generated: 2016_05_14-AM-07_38_27
Last ObjectModification: 2015_12_26-PM-02_12_41

Theory : list_1


Home Index