diff --git a/src/Plugin/TypeCheck/Nat/Simple/UnNomEq.hs b/src/Plugin/TypeCheck/Nat/Simple/UnNomEq.hs
--- a/src/Plugin/TypeCheck/Nat/Simple/UnNomEq.hs
+++ b/src/Plugin/TypeCheck/Nat/Simple/UnNomEq.hs
@@ -1,17 +1,29 @@
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ViewPatterns #-}
 {-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
 
 module Plugin.TypeCheck.Nat.Simple.UnNomEq (unNomEq) where
 
 import GHC.Tc.Types.Constraint (Ct, ctEvidence, ctEvPred)
-import GHC.Core.Type (Type)
+-- import GHC.Core.Type (Type)
 import GHC.Core.Predicate(Pred(..), EqRel(..), classifyPredType)
 import GHC.Utils.Outputable (ppr, text, (<+>))
 import Control.Monad.Try (Try, throw)
 import Data.Log (IsSDoc, fromSDoc)
 
+import GHC.Core.TyCo.Rep (Type(..))
+import GHC.Core.TyCon
+
+import GHC.Types.Name
+import GHC.Builtin.Types
+
 unNomEq :: (Monoid w, IsSDoc e) => Ct -> Try e w (Type, Type)
 unNomEq ct = case classifyPredType . ctEvPred $ ctEvidence ct of
 	EqPred NomEq l r -> pure (l, r)
+	IrredPred pt -> case pt of
+		TyConApp (nameStableString . tyConName ->
+				"$base$GHC.TypeError$Assert") [c, _e] ->
+			pure (c, TyConApp promotedTrueDataCon [])
+		_ -> throw . fromSDoc $ text "unNomEq: IrredPred" <+> ppr pt
 	_ -> throw . fromSDoc
 		$ text "unNomEq: no match to EqPred NomEq l r:" <+> ppr ct
diff --git a/typecheck-plugin-nat-simple.cabal b/typecheck-plugin-nat-simple.cabal
--- a/typecheck-plugin-nat-simple.cabal
+++ b/typecheck-plugin-nat-simple.cabal
@@ -1,13 +1,13 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.34.4.
+-- This file has been generated from package.yaml by hpack version 0.35.1.
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: c6e98b9ead49955ec8ae18665ed86d4db561b486b59685e673a22bdaac153161
+-- hash: a386dfeb25b891bd8c55323858f99e1f63f665d6c90dfc86b8eb6b4f78053dd6
 
 name:           typecheck-plugin-nat-simple
-version:        0.1.0.8
+version:        0.1.0.9
 synopsis:       Simple type check plugin which calculate addition, subtraction and less-or-equal-than
 description:    Please see the README on GitHub at <https://github.com/YoshikuniJujo/typecheck-plugin-nat-simple#readme>
 category:       Compiler Plugin