Nuprl Lemma : st-subst_wf
[st:SimpleType]. [subst:{a:Atom| (a 
st-vars(st))} 
SimpleType]. (st-subst(subst;st) SimpleType)
Proof not projected
Definitions occuring in Statement :
st-subst: st-subst(subst;st),
st-vars: st-vars(st),
simple_type: SimpleType,
uall: [x:A]. B[x],
member: t T,
set: {x:A| B[x]} ,
function: x:A B[x],
atom: Atom,
l_member: (x l)
Definitions :
guard: {T},
or: P 
Q,
so_lambda: 
x.t[x],
implies: P 
Q,
all: x:A. B[x],
st-subst: st-subst(subst;st),
member: t T,
st-vars: st-vars(st),
simple_type: SimpleType,
uall: [x:A]. B[x],
and: P 
Q,
iff: P 
Q,
rev_implies: P Q,
so_apply: x[s],
uimplies: b supposing a,
prop: 
,
st_class: st_class(kind),
st_list: st_list(kind),
st_union: st_union(left;right),
st_prod: st_prod(fst;snd),
st_arrow: st_arrow(domain;range),
st_const: st_const(ty),
st_var: st_var(name)
Lemmas :
st_class_wf,
st_list_wf,
st_union_wf,
st_prod_wf,
l-union_wf,
st-vars_wf,
atom-deq_wf,
member-union,
subtype_rel_self,
subtype_rel_sets,
subtype_rel_function,
st_arrow_wf,
st_const_wf,
l_member_wf,
simple_type_wf
\mforall{}[st:SimpleType]. \mforall{}[subst:\{a:Atom| (a \mmember{} st-vars(st))\} {}\mrightarrow{} SimpleType].
(st-subst(subst;st) \mmember{} SimpleType)
Date html generated:
2012_01_23-PM-12_52_31
Last ObjectModification:
2011_12_05-PM-12_41_34
Home
Index