| C.ACast (_,va,ty) -> C.Cast (deannotate_term va, deannotate_term ty)
| C.AProd (_,name,so,ta) ->
C.Prod (name, deannotate_term so, deannotate_term ta)
| C.ACast (_,va,ty) -> C.Cast (deannotate_term va, deannotate_term ty)
| C.AProd (_,name,so,ta) ->
C.Prod (name, deannotate_term so, deannotate_term ta)