+(* a metasenv is a list of declarations of metas *)
+and conjecture = int * context * term
+and metasenv = conjecture list
+
+(* a metasenv is a list of declarations of metas *)
+and annconjecture = id * int * anncontext * annterm
+and annmetasenv = annconjecture list
+