---

{ [x:st_exp{i:l}()]. ste_ap-fun(x)  st_exp{i:l}() supposing ste_ap?(x) }

{ Proof }

---

Definitions occuring in Statement :  ste_ap-fun: ste_ap-fun(x),  ste_ap?: ste_ap?(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],  st-constant: st-constant{i:l}(Info),  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_ap?: ste_ap?(x),  uall: [x:A]. B[x],  ste_ap-fun: ste_ap-fun(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_ap?_wf,  st_exp_wf,  true_wf,  false_wf

---

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


Date html generated: 2011_08_17-PM-05_07_13
Last ObjectModification: 2011_02_04-PM-01_29_26

Home Index