Nuprl Lemma : reduce_tl_cons_lemma

b,a:Top.  (tl([a b]) b)


Proof




Definitions occuring in Statement :  tl: tl(l) cons: [a b] top: Top all: x:A. B[x] sqequal: t
Definitions unfolded in proof :  member: t ∈ T all: x:A. B[x] tl: tl(l) cons: [a b] pi2: snd(t)
Lemmas referenced :  top_wf
Rules used in proof :  lemma_by_obid hypothesis cut lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution sqequalRule

Latex:
\mforall{}b,a:Top.    (tl([a  /  b])  \msim{}  b)



Date html generated: 2019_06_20-PM-00_38_18
Last ObjectModification: 2018_10_07-PM-00_42_22

Theory : list_0


Home Index