val list_uniq: 'a list -> 'a list (* uniq unix filter on lists *)
+ (** @return tl tail of a list starting at a given element
+ * @param eq equality to be used, defaults to physical equality (==)
+ * @raise Not_found *)
+val list_tl_at: ?equality:('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
+
(** @raise Failure *)
val unopt: 'a option -> 'a
val get_proof_status: MatitaTypes.status -> ProofEngineTypes.status
val get_proof_metasenv: MatitaTypes.status -> Cic.metasenv
val get_proof_context: MatitaTypes.status -> Cic.context
+val get_proof_conclusion: MatitaTypes.status -> Cic.term
val get_proof_aliases: MatitaTypes.status -> DisambiguateTypes.environment
(** given the base name of an image, returns its full path *)