| Cic.Prod (Cic.Name n, s, t) ->
PT.Binder (`Forall, (PT.Ident (n,None), Some (aux c s)),
aux (Some (Cic.Name n, Cic.Decl s)::c) t)
| Cic.Prod (Cic.Name n, s, t) ->
PT.Binder (`Forall, (PT.Ident (n,None), Some (aux c s)),
aux (Some (Cic.Name n, Cic.Decl s)::c) t)