---

{ [x:Pi_term]. pinew-name(x)  Name supposing pinew?(x) }

{ Proof }

---

Definitions occuring in Statement :  pinew-name: pinew-name(x),  pinew?: pinew?(x),  pi_term: Pi_term,  name: Name,  assert: b,  uimplies: b supposing a,  uall: [x:A]. B[x],  member: t  T
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  assert: b,  pinew?: pinew?(x),  member: t  T,  pinew-name: pinew-name(x),  implies: P  Q,  bfalse: ff,  btrue: tt,  ifthenelse: if b then t else f fi ,  pi_term: Pi_term,  unit: Unit,  false: False,  it: ,  pizero: 0,  prop: ,  picomm: pre.body,  pioption: (left + right),  pipar: (left | right),  pirep: !body,  pinew: (new name. body)
Lemmas :  pi_term_wf,  false_wf,  true_wf,  assert_wf,  pinew?_wf

---

\mforall{}[x:Pi\_term].  pinew-name(x)  \mmember{}  Name  supposing  \muparrow{}pinew?(x)


Date html generated: 2011_08_17-PM-06_45_00
Last ObjectModification: 2011_06_18-PM-12_15_05

Home Index