---

{ [t,x:Name]. [P:Pi_term].  (pi-replace(t;x;P)  Pi_term) }

{ Proof }

---

Definitions occuring in Statement :  pi-replace: pi-replace(t;x;P),  pi_term: Pi_term,  name: Name,  uall: [x:A]. B[x],  member: t  T
Definitions :  uall: [x:A]. B[x],  member: t  T,  pi-replace: pi-replace(t;x;P),  let: let,  so_lambda: so_lambda(x,y,z.t[x; y; z]),  so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),  so_lambda: x y.t[x; y],  so_apply: x[s1;s2;s3],  so_apply: x[s1;s2;s3;s4],  so_apply: x[s1;s2]
Lemmas :  pi_term_ind_wf,  pizero_wf,  picomm_wf,  prefix-replace_wf,  pi_prefix_wf,  pioption_wf,  pipar_wf,  pirep_wf,  pinew_wf,  ifthenelse_wf,  name_eq_wf,  pi_term_wf,  name_wf

---

\mforall{}[t,x:Name].  \mforall{}[P:Pi\_term].    (pi-replace(t;x;P)  \mmember{}  Pi\_term)


Date html generated: 2011_08_17-PM-06_48_58
Last ObjectModification: 2011_06_18-PM-12_21_42

Home Index