| Context of qid option (* context: Some = last node, None = root *)
| Block of id * term (* block opener: name, type *)
| Decl of id * term (* declaration: name, type *)
| Context of qid option (* context: Some = last node, None = root *)
| Block of id * term (* block opener: name, type *)
| Decl of id * term (* declaration: name, type *)