type lc_kind = Irl of int | Ctx of term list
and local_context = int * lc_kind (* shift (0 -> no shift),
type lc_kind = Irl of int | Ctx of term list
and local_context = int * lc_kind (* shift (0 -> no shift),
and term =
| Rel of int (* DeBruijn index, 1 based *)
| Meta of int * local_context
and term =
| Rel of int (* DeBruijn index, 1 based *)
| Meta of int * local_context