match (R.whd context ty) with
(C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) ->
PrimitiveTactics.apply_tac ~status:(proof,goal)
match (R.whd context ty) with
(C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) ->
PrimitiveTactics.apply_tac ~status:(proof,goal)