---

{ sc-Archive()  Expression }

{ Proof }

---

Definitions occuring in Statement :  sc-Archive: sc-Archive(),  expression: Expression,  member: t  T
Definitions :  sc-Archive: sc-Archive(),  expapply: fun(arg),  exppair: fst,snd,  expbase: val,  all: x:A. B[x],  function: x:A  B[x],  equal: s = t,  member: t  T,  token: "$token"
Lemmas :  expbase_wf,  exppair_wf,  expapply_wf

---

sc-Archive()  \mmember{}  Expression


Date html generated: 2010_08_27-PM-08_31_43
Last ObjectModification: 2010_06_24-AM-12_56_48

Home Index