There is much work on dependent types and most of it is affected by
the pioneering work by Martin-Löf [1]}.
Among many dependent type systems such as
\(\lambda ^\Pi \)  [2]}, The Calculus of
Constructions [3]}, and Edinburgh
LF [4]}, we base our work on \(\lambda \textrm {LF}\)   [5]}
(which is quite close to \(\lambda ^\Pi \)  and Edinburgh LF) due to its
simplicity. It is well known that dependent types are useful to
express detailed properties of data structures at the type level such
as the size of data structures [6]} and typed abstract syntax
trees [7]}, [8]}. The
vector addition discussed in Section  is also such an
example.
