---

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

{ Proof }

---

Definitions occuring in Statement :  pi-simple-subst: pi-simple-subst(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-simple-subst: pi-simple-subst(t;x;P),  member: t  T
Lemmas :  pi-rank-pi-simple-subst-aux,  pi-names_wf,  name_wf,  pi_term_wf

---

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


Date html generated: 2011_08_17-PM-06_51_45
Last ObjectModification: 2011_06_18-PM-12_24_26

Home Index