---

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

{ Proof }

---

Definitions occuring in Statement :  pi-subst: pi-subst(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-subst: pi-subst(t;x;p)
Lemmas :  pi-subst-aux_wf,  pi-names_wf,  pi_term_wf,  name_wf

---

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


Date html generated: 2011_08_17-PM-06_50_28
Last ObjectModification: 2011_06_18-PM-12_23_54

Home Index