Type
I(x) == 
i:I. D(i)(x)
x
y else Top fiy:Label. if x = f(y) d(y) else Top fi
D:(IDecl), x:Label, j:I, z:decl_type(D(i) for i I;x). z decl_type(D(j);x)d:Decl, f:(LabelLabel), x:Label, z:decl_type(d o f;f(x)). z decl_type(d;x)| def | decl | Decl == LabelType |
| def | dall | D(i) for i I(x) == i:I. D(i)(x) |
| def | dbase | x:y(a) == if a = x y else Top fi |
| def | rename_decl | d o f(x) == y:Label. if x = f(y) d(y) else Top fi |
| def | decl_type | decl_type(d;x) == d(x) |
| THM | dall_subtype | D:(IDecl), x:Label, j:I, z:decl_type(D(i) for i I;x). z decl_type(D(j);x) |
| THM | rename_decl_subtype | d:Decl, f:(LabelLabel), x:Label, z:decl_type(d o f;f(x)). z decl_type(d;x) |