DISP	env_df	Env( < f:f:* > ; < s:spec:* > )== Env Env== Env
ABS	env	Env == Atom t:Type J(t)
ML	env_soft	add_soft_abs ``env``;;
DISP	env_update_df	< en:en:* > {( < v:atom:* > : < tv:jtype:* > ) - > < o:o:* > } == < en > {( < v > : < tv > ) - > < o > }
ABS	env_update	en{(v:tv) - > o} == w,tw.if v =a w (tv =t tw) then o else en w tw fi
THM	env_update_wf	f:Atom . s:Spec. en:Env. v:Atom. t:Type. o:J(t). en{(v:t) - > o} Env

the other theories