C.ACurrentProof
("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params)
| C.InductiveDefinition (tys,params,paramsno) ->
C.ACurrentProof
("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params)
| C.InductiveDefinition (tys,params,paramsno) ->