---

{ [locs:Id List]. (sc-Inputs(locs)  BaseDef) }

{ Proof }

---

Definitions occuring in Statement :  sc-Inputs: sc-Inputs(locs),  base-deriv: BaseDef,  Id: Id,  uall: [x:A]. B[x],  member: t  T,  list: type List
Definitions :  uall: [x:A]. B[x],  member: t  T,  sc-Inputs: sc-Inputs(locs)
Lemmas :  BaseDef_wf,  int_wf_limited,  btrue_wf,  Id_wf

---

\mforall{}[locs:Id  List].  (sc-Inputs(locs)  \mmember{}  BaseDef)


Date html generated: 2011_08_17-PM-06_33_24
Last ObjectModification: 2011_06_18-AM-11_56_53

Home Index