(* depend on new ones. *)
and conjecture = int * context * term
and metasenv = conjecture list
+and substitution = (int * (context * term * term)) list
+
+
(* a metasenv is a list of declarations of metas in declarations *)
(* order (i.e. [oldest ; ... ; newest]). Older variables can not *)