let metano,context,ty = CicUtil.lookup_meta goal metasenv in
match (R.whd context ty) with
(C.Appl [(C.MutInd (uri, 0, [])); _; _; _])
when LibraryObjects.is_eq_URI uri ->
ProofEngineTypes.apply_tactic
(PrimitiveTactics.apply_tac
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
match (R.whd context ty) with
(C.Appl [(C.MutInd (uri, 0, [])); _; _; _])
when LibraryObjects.is_eq_URI uri ->
ProofEngineTypes.apply_tactic
(PrimitiveTactics.apply_tac