---

{ [s:(Name  Name) List]. [x:Name].  (name-subst(s;x)  Name) }

{ Proof }

---

Definitions occuring in Statement :  name-subst: name-subst(s;x),  name: Name,  uall: [x:A]. B[x],  member: t  T,  product: x:A  B[x],  list: type List
Definitions :  uall: [x:A]. B[x],  member: t  T,  name-subst: name-subst(s;x)
Lemmas :  apply-alist_wf,  name-deq_wf,  name_wf

---

\mforall{}[s:(Name  \mtimes{}  Name)  List].  \mforall{}[x:Name].    (name-subst(s;x)  \mmember{}  Name)


Date html generated: 2011_08_10-AM-07_42_22
Last ObjectModification: 2011_06_18-AM-08_09_37

Home Index