type lc_kind = Irl of int | Ctx of term list
and local_context = int * lc_kind (* shift (0 -> no shift),
- subst (None means id) *)
+ subst (Irl n means id of
+ length n) *)
and term =
| Rel of int (* DeBruijn index, 1 based *)
| Meta of int * local_context