Nuprl Lemma : reverse_nil_lemma

rev([]) []


Proof




Definitions occuring in Statement :  reverse: rev(as) nil: [] sqequal: t
Definitions unfolded in proof :  reverse: rev(as) all: x:A. B[x] member: t ∈ T top: Top
Lemmas referenced :  rev_app_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:
rev([])  \msim{}  []



Date html generated: 2016_05_14-AM-06_54_30
Last ObjectModification: 2015_12_26-PM-00_19_34

Theory : list_0


Home Index