{ 
[x:SimpleType]. st_const-ty(x) 
Type supposing 
st_const?(x) }
{ Proof }
Definitions occuring in Statement :
st_const-ty: st_const-ty(x),
st_const?: st_const?(x),
simple_type: SimpleType,
assert: b,
uimplies: b supposing a,
uall: [x:A]. B[x],
member: t T,
universe: Type
Definitions :
true: True,
simple_type_ind: simple_type_ind,
apply: f a,
it: 
,
false: False,
simple_type_ind_st_class: simple_type_ind_st_class_compseq_tag_def,
simple_type_ind_st_list: simple_type_ind_st_list_compseq_tag_def,
simple_type_ind_st_union: simple_type_ind_st_union_compseq_tag_def,
simple_type_ind_st_prod: simple_type_ind_st_prod_compseq_tag_def,
simple_type_ind_st_arrow: simple_type_ind_st_arrow_compseq_tag_def,
simple_type_ind_st_const: simple_type_ind_st_const_compseq_tag_def,
simple_type_ind_st_var: simple_type_ind_st_var_compseq_tag_def,
set: {x:A| B[x]} ,
product: x:A 
B[x],
atom: Atom,
union: left + right,
rec: rec(x.A[x]),
implies: P 
Q,
function: x:A 
B[x],
all: x:A. B[x],
st_const?: st_const?(x),
uall: [x:A]. B[x],
universe: Type,
st_const-ty: st_const-ty(x),
axiom: Ax,
uimplies: b supposing a,
isect: 
x:A. B[x],
assert: b,
prop: 
,
simple_type: SimpleType,
equal: s = t,
member: t T
Lemmas :
assert_wf,
st_const?_wf,
simple_type_wf,
true_wf,
false_wf
\mforall{}[x:SimpleType]. st\_const-ty(x) \mmember{} Type supposing \muparrow{}st\_const?(x)
Date html generated:
2011_08_17-PM-04_45_03
Last ObjectModification:
2011_02_06-PM-04_10_37
Home
Index