val lift: int -> int -> Cic.annterm -> Cic.annterm
+val fake_annotate: Cic.id -> Cic.context -> Cic.term -> Cic.annterm
+
val mk_pattern: int -> Cic.annterm -> Cic.annterm
val get_clears:
Cic.context * string list
val clear: Cic.context -> string -> Cic.context
+
+val elim_inferred_type:
+ Cic.context -> Cic.term -> Cic.term -> Cic.term -> Cic.term -> Cic.term
+
+val does_not_occur: Cic.annterm -> bool