| CicNotationPt.Theorem (flav, n, t, ty_opt) ->
let ty_opt =
match ty_opt with None -> None | Some ty -> Some (freshen_term ty)
in
CicNotationPt.Theorem (flav, n, freshen_term t, ty_opt)
| CicNotationPt.Record (params, n, ty, fields) ->
| CicNotationPt.Theorem (flav, n, t, ty_opt) ->
let ty_opt =
match ty_opt with None -> None | Some ty -> Some (freshen_term ty)
in
CicNotationPt.Theorem (flav, n, freshen_term t, ty_opt)
| CicNotationPt.Record (params, n, ty, fields) ->