(Cic.id, anntypes) Hashtbl.t * (* ids_to_inner_types *)
(Cic.id, Cic.conjecture) Hashtbl.t * (* ids_to_conjectures *)
(Cic.id, Cic.hypothesis) Hashtbl.t (* ids_to_hypotheses *)
+
+val asequent_of_sequent :
+ Cic.metasenv -> (* metasenv *)
+ Cic.conjecture -> (* conjecture *)
+ Cic.annconjecture * (* annotated conjecture *)
+ (Cic.id, Cic.term) Hashtbl.t * (* ids_to_terms *)
+ (Cic.id, Cic.id option) Hashtbl.t * (* ids_to_father_ids *)
+ (Cic.id, string) Hashtbl.t * (* ids_to_inner_sorts *)
+ (Cic.id, Cic.hypothesis) Hashtbl.t (* ids_to_hypotheses *)