---

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

{ Proof }

---

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

---

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


Date html generated: 2011_08_17-PM-06_50_37
Last ObjectModification: 2011_06_18-PM-12_24_10

Home Index