---

{ [x,y,z,v:Name].  (pi-example(x;y;z;v)  Pi_term) }

{ Proof }

---

Definitions occuring in Statement :  pi-example: pi-example(x;y;z;v),  pi_term: Pi_term,  name: Name,  uall: [x:A]. B[x],  member: t  T
Definitions :  uall: [x:A]. B[x],  member: t  T,  pi-example: pi-example(x;y;z;v)
Lemmas :  pipar_wf,  pinew_wf,  picomm_wf,  pisend_wf,  pizero_wf,  pircv_wf,  name_wf

---

\mforall{}[x,y,z,v:Name].    (pi-example(x;y;z;v)  \mmember{}  Pi\_term)


Date html generated: 2011_08_17-PM-06_46_20
Last ObjectModification: 2011_06_18-PM-12_17_10

Home Index