let ty,_ = CicTypeChecker.type_of_aux' [] context s CicUniv.oblivion_ugraph in
"(let " ^ ppname b ^ " = " ^ pp ~in_type:false s context ^ " in " ^
pp ~in_type t ((Some (b,Cic.Def (s,Some ty)))::context) ^ ")"
let ty,_ = CicTypeChecker.type_of_aux' [] context s CicUniv.oblivion_ugraph in
"(let " ^ ppname b ^ " = " ^ pp ~in_type:false s context ^ " in " ^
pp ~in_type t ((Some (b,Cic.Def (s,Some ty)))::context) ^ ")"