{ 
[x:esharp_exp()]
esharplambda-body(x) 
esharp_exp() supposing 
esharplambda?(x) }
{ Proof }
Definitions occuring in Statement :
esharplambda-body: esharplambda-body(x),
esharplambda?: esharplambda?(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],
esharplambda?: esharplambda?(x),
uall: [x:A]. B[x],
esharplambda-body: esharplambda-body(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,
esharplambda?_wf,
esharp_exp_wf,
true_wf,
false_wf
\mforall{}[x:esharp\_exp()]. esharplambda-body(x) \mmember{} esharp\_exp() supposing \muparrow{}esharplambda?(x)
Date html generated:
2011_08_17-PM-05_55_37
Last ObjectModification:
2011_02_03-PM-04_44_10
Home
Index