{ 
[s:Atom 
SimpleType]. [st:SimpleType].
st-kind(st-subst(s;st)) ~ st-kind(st) supposing 
st_var?(st) }
{ Proof }
Definitions occuring in Statement :
st-kind: st-kind(st),
st-subst: st-subst(subst;st),
st_var?: st_var?(x),
simple_type: SimpleType,
assert: b,
uimplies: b supposing a,
uall: [x:A]. B[x],
not: A,
function: x:A B[x],
atom: Atom,
sqequal: s ~ t
Definitions :
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,
natural_number: $n,
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,
false: False,
implies: P 
Q,
true: True,
simple_type_ind_st_var: simple_type_ind_st_var_compseq_tag_def,
st-kind: st-kind(st),
st-subst: st-subst(subst;st),
set: {x:A| B[x]} ,
product: x:A 
B[x],
union: left + right,
rec: rec(x.A[x]),
universe: Type,
st_var?: st_var?(x),
all: x:A. B[x],
equal: s = t,
so_lambda: 
x.t[x],
function: x:A B[x],
atom: Atom,
sqequal: s ~ t,
uall: [x:A]. B[x],
simple_type: SimpleType,
uimplies: b supposing a,
assert: b,
prop: 
,
not: A,
member: t 
T,
isect: 
x:A. B[x],
Auto: Error :Auto,
Try: Error :Try,
CollapseTHEN: Error :CollapseTHEN,
RepUR: Error :RepUR,
CollapseTHENA: Error :CollapseTHENA,
RepeatFor: Error :RepeatFor
Lemmas :
st_var?_wf,
uall_wf,
assert_wf,
simple_type_wf,
true_wf,
false_wf,
not_wf
\mforall{}[s:Atom {}\mrightarrow{} SimpleType]. \mforall{}[st:SimpleType].
st-kind(st-subst(s;st)) \msim{} st-kind(st) supposing \mneg{}\muparrow{}st\_var?(st)
Date html generated:
2011_08_17-PM-04_59_08
Last ObjectModification:
2011_02_07-PM-11_37_36
Home
Index