Nuprl Lemma : id-member-normal-form
∀[x,L:Top]. (rec-case(L) of [] => ff | a::_ => r.if a=2 x then tt else r ~ x ∈b L))
Proof
Definitions occuring in Statement :
id-deq: IdDeq,
deq-member: x ∈b L),
list_ind: list_ind,
atom_eq: atomeqn def,
bfalse: ff,
btrue: tt,
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t
Lemmas :
lifting-strict-atom_eq2,
has-value_wf_base,
base_wf,
top_wf
\mforall{}[x,L:Top]. (rec-case(L) of [] => ff | a::$_{}$ => r.if a=2 x then tt else r \msim{} \000Cx \mmember{}\msubb{} L))
Date html generated:
2015_07_17-AM-09_15_11
Last ObjectModification:
2015_01_28-AM-07_53_22
Home
Index