---

{ [x:st_exp{i:l}()]
    ste_const-val(x)  st-constant{i:l} supposing ste_const?(x) }

{ Proof }

---

Definitions occuring in Statement :  ste_const-val: ste_const-val(x),  ste_const?: ste_const?(x),  st_exp: st_exp{i:l}(),  assert: b,  uimplies: b supposing a,  uall: [x:A]. B[x],  member: t  T
Definitions :  true: True,  st_exp_ind: st_exp_ind,  apply: f a,  it: ,  false: False,  st_exp_ind_ste_lambda: st_exp_ind_ste_lambda_compseq_tag_def,  st_exp_ind_ste_ap: st_exp_ind_ste_ap_compseq_tag_def,  st_exp_ind_ste_const: st_exp_ind_ste_const_compseq_tag_def,  st_exp_ind_ste_var: st_exp_ind_ste_var_compseq_tag_def,  simple_type: Error :simple_type,  set: {x:A| B[x]} ,  product: x:A  B[x],  universe: Type,  atom: Atom,  union: left + right,  rec: rec(x.A[x]),  implies: P  Q,  function: x:A  B[x],  all: x:A. B[x],  ste_const?: ste_const?(x),  uall: [x:A]. B[x],  st-constant: st-constant{i:l}(Info),  ste_const-val: ste_const-val(x),  axiom: Ax,  uimplies: b supposing a,  isect: x:A. B[x],  assert: b,  prop: ,  st_exp: st_exp{i:l}(),  equal: s = t,  member: t  T
Lemmas :  assert_wf,  ste_const?_wf,  st_exp_wf,  true_wf,  false_wf

---

\mforall{}[x:st\_exp\{i:l\}()].  ste\_const-val(x)  \mmember{}  st-constant\{i:l\}  supposing  \muparrow{}ste\_const?(x)


Date html generated: 2011_08_17-PM-05_06_33
Last ObjectModification: 2011_02_04-PM-01_29_32

Home Index