match obj with
Cic.InductiveDefinition ([_,_,sort,[_,ty]],params,paramsno,_) ->
assert (params = []); (* general case not implemented *)
match obj with
Cic.InductiveDefinition ([_,_,sort,[_,ty]],params,paramsno,_) ->
assert (params = []); (* general case not implemented *)