Nuprl Lemma : list_to_set_nil_lemma
∀eq:Top. (list-to-set(eq;[]) ~ [])
Proof
Definitions occuring in Statement :
list-to-set: list-to-set(eq;L),
nil: [],
top: Top,
all: ∀x:A. B[x],
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
list-to-set: list-to-set(eq;L),
l-union: as ⋃ bs,
reduce: reduce(f;k;as),
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
Latex:
\mforall{}eq:Top. (list-to-set(eq;[]) \msim{} [])
Date html generated:
2016_05_14-PM-03_25_44
Last ObjectModification:
2015_12_26-PM-06_22_42
Theory : decidable!equality
Home
Index