---

{ [me,s:Name]. [avoid:Name List].  (maybe-new-local(me;s;avoid)  Name) }

{ Proof }

---

Definitions occuring in Statement :  maybe-new-local: maybe-new-local(me;s;avoid),  name: Name,  uall: [x:A]. B[x],  member: t  T,  list: type List
Definitions :  uall: [x:A]. B[x],  name: Name,  member: t  T,  maybe-new-local: maybe-new-local(me;s;avoid),  prop:
Lemmas :  append_wf,  name_wf,  maybe-new_wf,  not_wf,  l_member_wf

---

\mforall{}[me,s:Name].  \mforall{}[avoid:Name  List].    (maybe-new-local(me;s;avoid)  \mmember{}  Name)


Date html generated: 2011_08_17-PM-06_58_52
Last ObjectModification: 2011_06_18-PM-12_38_00

Home Index