{ 
[x:SimpleType]. st_union-right(x) 
SimpleType supposing 
st_union?(x) }
{ Proof }
Definitions occuring in Statement :
st_union-right: st_union-right(x),
st_union?: st_union?(x),
simple_type: SimpleType,
assert: b,
uimplies: b supposing a,
uall: [x:A]. B[x],
member: t T
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],
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],
st_union?: st_union?(x),
uall: [x:A]. B[x],
st_union-right: st_union-right(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_union?_wf,
simple_type_wf,
true_wf,
false_wf
\mforall{}[x:SimpleType]. st\_union-right(x) \mmember{} SimpleType supposing \muparrow{}st\_union?(x)
Date html generated:
2011_08_17-PM-04_48_13
Last ObjectModification:
2011_02_06-PM-04_15_37
Home
Index