*)
let eliminator_type =
FreshNamesGenerator.mk_fresh_names [] [] [] eliminator_type in
let eliminator_body =
FreshNamesGenerator.mk_fresh_names [] [] [] eliminator_body in
(*
*)
let eliminator_type =
FreshNamesGenerator.mk_fresh_names [] [] [] eliminator_type in
let eliminator_body =
FreshNamesGenerator.mk_fresh_names [] [] [] eliminator_body in
(*