generate_exact seed t id name ~ids_to_inner_types
else raise Not_a_proof
| C.AMutInd (id,uri,i,exp_named_subst) -> raise Not_a_proof
| C.AMutConstruct (id,uri,i,j,exp_named_subst) as t ->
let sort = Hashtbl.find ids_to_inner_sorts id in
generate_exact seed t id name ~ids_to_inner_types
else raise Not_a_proof
| C.AMutInd (id,uri,i,exp_named_subst) -> raise Not_a_proof
| C.AMutConstruct (id,uri,i,j,exp_named_subst) as t ->
let sort = Hashtbl.find ids_to_inner_sorts id in