{ [env:E#Env]. [x:Atom].  (esharp-base-wf(env;x)  ) }

{ Proof }



Definitions occuring in Statement :  esharp-base-wf: esharp-base-wf(env;x),  esharp-env: E#Env,  bool: ,  uall: [x:A]. B[x],  member: t  T,  atom: Atom
Definitions :  uall: [x:A]. B[x],  esharp-env: E#Env,  member: t  T,  esharp-base-wf: esharp-base-wf(env;x),  and: P  Q,  prop:
Lemmas :  apply-alist_wf,  atom-deq_wf,  base-deriv_wf,  combinator-def_wf,  classderiv_wf,  cdv-wf_wf,  length_wf1,  cdv-types_wf,  btrue_wf,  bfalse_wf

\mforall{}[env:E\#Env].  \mforall{}[x:Atom].    (esharp-base-wf(env;x)  \mmember{}  \mBbbB{})


Date html generated: 2011_08_17-PM-04_31_32
Last ObjectModification: 2011_06_18-AM-11_42_52

Home Index