| C.MutCase (uri,i,outtype,term,pl) ->
(match CicReduction.whd ~subst context term with
C.Rel m when List.mem m safes || m = x ->
| C.MutCase (uri,i,outtype,term,pl) ->
(match CicReduction.whd ~subst context term with
C.Rel m when List.mem m safes || m = x ->