Nuprl Lemma : bound_in_prefix_wf

[pre:pi_prefix()]. (bound_in_prefix(pre) ∈ Name List)


Proof




Definitions occuring in Statement :  bound_in_prefix: bound_in_prefix(pre) pi_prefix: pi_prefix() name: Name list: List uall: [x:A]. B[x] member: t ∈ T
Lemmas :  pi_prefix_ind_wf_simple list_wf name_wf nil_wf cons_wf pi_prefix_wf

Latex:
\mforall{}[pre:pi\_prefix()].  (bound\_in\_prefix(pre)  \mmember{}  Name  List)



Date html generated: 2015_07_23-AM-11_34_01
Last ObjectModification: 2015_01_29-AM-00_54_53

Home Index