(* [typ] will be the type of the variable *)
val mk_fresh_name :
Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
+
+(* clean_dummy_dependent_types term *)
+(* returns a copy of [term] where every dummy dependent product *)
+(* have been replaced with a non-dependent product and where *)
+(* dummy let-ins have been removed. *)
+val clean_dummy_dependent_types : Cic.term -> Cic.term