---

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

{ Proof }

---

Definitions occuring in Statement :  pi-replace: pi-replace(t;x;P),  pi-rank: pi-rank(p),  pi_term: Pi_term,  name: Name,  uall: [x:A]. B[x],  int: ,  equal: s = t
Definitions :  uall: [x:A]. B[x],  pi-rank: pi-rank(p),  pi-replace: pi-replace(t;x;P),  member: t  T,  all: x:A. B[x],  prop: ,  implies: P  Q,  so_lambda: x.t[x],  let: let,  so_apply: x[s],  guard: {T},  nat:
Lemmas :  pi_term-induction,  pi-rank_wf,  pi-replace_wf,  nat_wf,  pi_prefix_wf,  pi_term_wf,  name_wf

---

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


Date html generated: 2011_08_17-PM-06_49_07
Last ObjectModification: 2011_06_18-PM-12_22_02

Home Index