NCic.Inductive (true,leftno,[itl],_) ->
List.map (fun s-> mk_elim status uri leftno itl (ast_of_sort s) (`Elim s))
(NCic.Prop::
NCic.Inductive (true,leftno,[itl],_) ->
List.map (fun s-> mk_elim status uri leftno itl (ast_of_sort s) (`Elim s))
(NCic.Prop::