+ | C.AMutCase (id, uri, tyno, outty, arg, cases) as v ->
+ begin match Cn.mk_ind st.context id uri tyno outty arg cases with
+ | None -> [T.LetIn (name, v, dtext)]
+ | Some v -> mk_fwd_proof st dtext name v
+ end
+ | v ->
+ [T.LetIn (name, v, dtext)]