---

{ [x:esharp_exp()]
    esharpapply-fun(x)  esharp_exp() supposing esharpapply?(x) }

{ Proof }

---

Definitions occuring in Statement :  esharpapply-fun: esharpapply-fun(x),  esharpapply?: esharpapply?(x),  esharp_exp: esharp_exp(),  assert: b,  uimplies: b supposing a,  uall: [x:A]. B[x],  member: t  T
Definitions :  true: True,  esharp_exp_ind: esharp_exp_ind,  apply: f a,  it: ,  false: False,  esharp_exp_ind_esharplet: esharp_exp_ind_esharplet_compseq_tag_def,  esharp_exp_ind_esharplambda: esharp_exp_ind_esharplambda_compseq_tag_def,  esharp_exp_ind_esharpapply: esharp_exp_ind_esharpapply_compseq_tag_def,  esharp_exp_ind_esharpop: esharp_exp_ind_esharpop_compseq_tag_def,  esharp_exp_ind_esharpbasic: esharp_exp_ind_esharpbasic_compseq_tag_def,  esharp_exp_ind_esharpvar: esharp_exp_ind_esharpvar_compseq_tag_def,  esharp-lhs: E#Lhs,  set: {x:A| B[x]} ,  product: x:A  B[x],  base: Base,  atom: Atom,  union: left + right,  universe: Type,  rec: rec(x.A[x]),  implies: P  Q,  function: x:A  B[x],  all: x:A. B[x],  esharpapply?: esharpapply?(x),  uall: [x:A]. B[x],  esharpapply-fun: esharpapply-fun(x),  axiom: Ax,  uimplies: b supposing a,  isect: x:A. B[x],  assert: b,  prop: ,  esharp_exp: esharp_exp(),  equal: s = t,  member: t  T
Lemmas :  assert_wf,  esharpapply?_wf,  esharp_exp_wf,  true_wf,  false_wf

---

\mforall{}[x:esharp\_exp()].  esharpapply-fun(x)  \mmember{}  esharp\_exp()  supposing  \muparrow{}esharpapply?(x)


Date html generated: 2011_08_17-PM-05_53_21
Last ObjectModification: 2011_02_03-PM-04_42_03

Home Index