| C.Cast (te,ty) -> C.Cast (restore_in_term te, restore_in_term ty)
| C.Prod (n,s,t) -> C.Prod (n, restore_in_term s, restore_in_term t)
| C.Lambda (n,s,t) -> C.Lambda (n, restore_in_term s, restore_in_term t)
| C.Cast (te,ty) -> C.Cast (restore_in_term te, restore_in_term ty)
| C.Prod (n,s,t) -> C.Prod (n, restore_in_term s, restore_in_term t)
| C.Lambda (n,s,t) -> C.Lambda (n, restore_in_term s, restore_in_term t)