diff --git a/kore/CHANGELOG.md b/kore/CHANGELOG.md
index d60552df3e..ea79d72fdc 100644
--- a/kore/CHANGELOG.md
+++ b/kore/CHANGELOG.md
@@ -22,7 +22,6 @@ All notable changes to this project will be documented in this file.
 
 ### Changed
 
-- Execution does not branch when evaluating the hooked `KEQUAL.eq` function.
 - Clarified the message accompanying the "substitution coverage" error.
 
 ### Fixed
diff --git a/kore/src/Kore/Builtin/Bool.hs b/kore/src/Kore/Builtin/Bool.hs
index ff95bece10..53d23341ea 100644
--- a/kore/src/Kore/Builtin/Bool.hs
+++ b/kore/src/Kore/Builtin/Bool.hs
@@ -14,8 +14,6 @@ module Kore.Builtin.Bool
     , extractBoolDomainValue
     , parse
     , termAndEquals
-    , termNotBool
-    , matchBool
       -- * Keys
     , orKey
     , andKey
@@ -210,26 +208,7 @@ termAndEquals unifyChildren a b =
         unification2 <- unifyChildren' termLike1 operand2
         let conditions = unification1 <> unification2
         pure (Pattern.withCondition termLike1 conditions)
-    worker _ _ = empty
 
-termNotBool
-    :: forall variable unifier
-    .  InternalVariable variable
-    => MonadUnify unifier
-    => TermSimplifier variable unifier
-    -> TermLike variable
-    -> TermLike variable
-    -> MaybeT unifier (Pattern variable)
-termNotBool unifyChildren a b =
-    worker a b <|> worker b a
-  where
-    worker termLike1 boolTerm
-      | Just BoolNot { operand } <- matchBoolNot termLike1
-      , isFunctionPattern termLike1
-      , Just value <- matchBool boolTerm
-      = lift $ do
-        let notValue = asInternal (termLikeSort boolTerm) (not value)
-        unifyChildren notValue operand
     worker _ _ = empty
 
 {- | Match a @BOOL.Bool@ builtin value.
@@ -255,20 +234,3 @@ matchBoolAnd (App_ symbol [operand1, operand2]) = do
     Monad.guard (hook2 == andKey)
     return BoolAnd { symbol, operand1, operand2 }
 matchBoolAnd _ = Nothing
-
-{- | The @BOOL.not@ hooked symbol applied to a @term@-type argument.
- -}
-data BoolNot term =
-    BoolNot
-        { symbol  :: !Symbol
-        , operand :: !term
-        }
-
-{- | Match the @BOOL.not@ hooked symbol.
- -}
-matchBoolNot :: TermLike variable -> Maybe (BoolNot (TermLike variable))
-matchBoolNot (App_ symbol [operand]) = do
-    hook2 <- (getHook . symbolHook) symbol
-    Monad.guard (hook2 == notKey)
-    return BoolNot { symbol, operand }
-matchBoolNot _ = Nothing
diff --git a/kore/src/Kore/Builtin/KEqual.hs b/kore/src/Kore/Builtin/KEqual.hs
index 9d86e7f442..36f32440b4 100644
--- a/kore/src/Kore/Builtin/KEqual.hs
+++ b/kore/src/Kore/Builtin/KEqual.hs
@@ -17,8 +17,6 @@ builtin modules.
 module Kore.Builtin.KEqual
     ( verifiers
     , builtinFunctions
-    , KEqual (..)
-    , termKEquals
       -- * keys
     , eqKey
     , neqKey
@@ -27,11 +25,6 @@ module Kore.Builtin.KEqual
 
 import Prelude.Kore
 
-import Control.Error
-    ( MaybeT
-    , hoistMaybe
-    )
-import qualified Control.Monad as Monad
 import qualified Data.Functor.Foldable as Recursive
 import qualified Data.HashMap.Strict as HashMap
 import Data.Map.Strict
@@ -45,9 +38,6 @@ import Data.Text
     ( Text
     )
 
-import Kore.Attribute.Hook
-    ( Hook (..)
-    )
 import qualified Kore.Attribute.Pattern as Attribute
 import qualified Kore.Builtin.Bool as Bool
 import Kore.Builtin.Builtin
@@ -56,22 +46,20 @@ import Kore.Builtin.Builtin
 import qualified Kore.Builtin.Builtin as Builtin
 import qualified Kore.Error
 import qualified Kore.Internal.OrPattern as OrPattern
-import Kore.Internal.Pattern
-    ( Pattern
-    )
 import qualified Kore.Internal.Pattern as Pattern
 import qualified Kore.Internal.SideCondition as SideCondition
-import Kore.Internal.Symbol
+    ( topTODO
+    )
 import Kore.Internal.TermLike
-import Kore.Step.Simplification.NotSimplifier
+import qualified Kore.Step.Simplification.And as And
+import qualified Kore.Step.Simplification.Ceil as Ceil
+import qualified Kore.Step.Simplification.Equals as Equals
+import qualified Kore.Step.Simplification.Not as Not
+import qualified Kore.Step.Simplification.Or as Or
 import Kore.Step.Simplification.Simplify
 import Kore.Syntax.Definition
     ( SentenceSymbol (..)
     )
-import Kore.Unification.Unify as Unify
-import Kore.Unification.Unify
-    ( MonadUnify
-    )
 
 verifiers :: Builtin.Verifiers
 verifiers =
@@ -137,8 +125,7 @@ builtinFunctions =
     ]
 
 evalKEq
-    :: forall variable simplifier
-    .  (InternalVariable variable, MonadSimplify simplifier)
+    :: (InternalVariable variable, MonadSimplify simplifier)
     => Bool
     -> CofreeF
         (Application Symbol)
@@ -147,24 +134,41 @@ evalKEq
     -> simplifier (AttemptedAxiom variable)
 evalKEq true (valid :< app) =
     case applicationChildren of
-        [t1, t2] -> Builtin.getAttemptedAxiom (evalEq t1 t2)
+        [t1, t2] -> evalEq t1 t2
         _ -> Builtin.wrongArity (if true then eqKey else neqKey)
   where
+    sideCondition = SideCondition.topTODO
+    false = not true
     sort = Attribute.patternSort valid
     Application { applicationChildren } = app
-    comparison x y
-        | true = x == y
-        | otherwise = x /= y
-    evalEq
-        :: TermLike variable
-        -> TermLike variable
-        -> MaybeT simplifier (AttemptedAxiom variable)
     evalEq termLike1 termLike2 = do
-        asConcrete1 <- hoistMaybe $ Builtin.toKey termLike1
-        asConcrete2 <- hoistMaybe $ Builtin.toKey termLike2
-        Builtin.appliedFunction
-            $ Bool.asPattern sort
-            $ comparison asConcrete1 asConcrete2
+        let pattern1 = Pattern.fromTermLike termLike1
+            pattern2 = Pattern.fromTermLike termLike2
+
+        defined1 <- Ceil.makeEvaluate sideCondition pattern1
+        defined2 <- Ceil.makeEvaluate sideCondition pattern2
+        defined <-
+            And.simplifyEvaluated Not.notSimplifier sideCondition defined1 defined2
+
+        equalTerms <-
+            Equals.makeEvaluateTermsToPredicate
+                termLike1
+                termLike2
+                sideCondition
+        let trueTerm = Bool.asInternal sort true
+            truePatterns = Pattern.withCondition trueTerm <$> equalTerms
+
+        notEqualTerms <- Not.simplifyEvaluatedPredicate equalTerms
+        let falseTerm = Bool.asInternal sort false
+            falsePatterns = Pattern.withCondition falseTerm <$> notEqualTerms
+
+        let undefinedResults = Or.simplifyEvaluated truePatterns falsePatterns
+        results <-
+            And.simplifyEvaluated Not.notSimplifier sideCondition defined undefinedResults
+        pure $ Applied AttemptedAxiomResults
+            { results
+            , remainders = OrPattern.bottom
+            }
 
 evalKIte
     :: forall variable simplifier
@@ -204,51 +208,3 @@ neqKey = "KEQUAL.neq"
 
 iteKey :: IsString s => s
 iteKey = "KEQUAL.ite"
-
-{- | The @KEQUAL.eq@ hooked symbol applied to @term@-type arguments.
- -}
-data KEqual term =
-    KEqual
-        { symbol :: !Symbol
-        , operand1, operand2 :: !term
-        }
-
-{- | Match the @KEQUAL.eq@ hooked symbol.
- -}
-matchKEqual :: TermLike variable -> Maybe (KEqual (TermLike variable))
-matchKEqual (App_ symbol [operand1, operand2]) = do
-    hook2 <- (getHook . symbolHook) symbol
-    Monad.guard (hook2 == eqKey)
-    return KEqual { symbol, operand1, operand2 }
-matchKEqual _ = Nothing
-
-termKEquals
-    :: forall variable unifier
-    .  InternalVariable variable
-    => MonadUnify unifier
-    => TermSimplifier variable unifier
-    -> NotSimplifier unifier
-    -> TermLike variable
-    -> TermLike variable
-    -> MaybeT unifier (Pattern variable)
-termKEquals unifyChildren (NotSimplifier notSimplifier) a b =
-    worker a b <|> worker b a
-  where
-    eraseTerm =
-        Pattern.fromCondition . Pattern.withoutTerm
-    worker termLike1 termLike2
-      | Just KEqual { operand1, operand2 } <- matchKEqual termLike1
-      , isFunctionPattern termLike1
-      , Just value2 <- Bool.matchBool termLike2
-      = lift $ do
-        solution <-
-            fmap OrPattern.fromPatterns
-            <$> Unify.gather
-            $ unifyChildren operand1 operand2
-        let solution' = fmap eraseTerm solution
-        finalSolution <-
-            if value2
-                then return solution'
-                else notSimplifier SideCondition.top solution'
-        Unify.scatter finalSolution
-    worker _ _ = empty
diff --git a/kore/src/Kore/Step/Simplification/AndTerms.hs b/kore/src/Kore/Step/Simplification/AndTerms.hs
index ca68469357..75326ee8bf 100644
--- a/kore/src/Kore/Step/Simplification/AndTerms.hs
+++ b/kore/src/Kore/Step/Simplification/AndTerms.hs
@@ -35,7 +35,6 @@ import qualified Data.Text.Prettyprint.Doc as Pretty
 
 import qualified Kore.Builtin.Bool as Builtin.Bool
 import qualified Kore.Builtin.Endianness as Builtin.Endianness
-import qualified Kore.Builtin.KEqual as Builtin.KEqual
 import qualified Kore.Builtin.List as Builtin.List
 import qualified Kore.Builtin.Map as Builtin.Map
 import qualified Kore.Builtin.Set as Builtin.Set
@@ -231,8 +230,6 @@ andEqualsFunctions notSimplifier = fmap mapEqualsFunctions
     , (BothT,   \_ _ _ -> constructorAndEqualsAssumesDifferentHeads, "constructorAndEqualsAssumesDifferentHeads")
     , (BothT,   \_ _ s -> overloadedConstructorSortInjectionAndEquals s, "overloadedConstructorSortInjectionAndEquals")
     , (BothT,   \_ _ s -> Builtin.Bool.termAndEquals s, "Builtin.Bool.termAndEquals")
-    , (BothT,   \_ _ s -> Builtin.Bool.termNotBool s, "Builtin.Bool.termNotBool")
-    , (EqualsT, \_ _ s -> Builtin.KEqual.termKEquals s notSimplifier, "Builtin.KEqual.termKEquals")
     , (BothT,   \_ _ _ -> Builtin.Endianness.unifyEquals, "Builtin.Endianness.unifyEquals")
     , (BothT,   \_ _ _ -> Builtin.Signedness.unifyEquals, "Builtin.Signedness.unifyEquals")
     , (BothT,   \_ _ s -> Builtin.Map.unifyEquals s, "Builtin.Map.unifyEquals")
diff --git a/kore/test/Test/Kore/Builtin/KEqual.hs b/kore/test/Test/Kore/Builtin/KEqual.hs
index be45c0f55e..ce2d8ec51d 100644
--- a/kore/test/Test/Kore/Builtin/KEqual.hs
+++ b/kore/test/Test/Kore/Builtin/KEqual.hs
@@ -3,7 +3,6 @@ module Test.Kore.Builtin.KEqual
     , test_kneq
     , test_KEqual
     , test_KIte
-    , test_KEqualSimplification
     ) where
 
 import Prelude.Kore
@@ -12,33 +11,10 @@ import Hedgehog
 import qualified Hedgehog.Gen as Gen
 import Test.Tasty
 
-import Control.Monad.Trans.Maybe
-    ( runMaybeT
-    )
 import qualified Data.Text as Text
 
-import qualified Kore.Builtin.KEqual as KEqual
-import Kore.Internal.Pattern
-    ( Pattern
-    )
 import qualified Kore.Internal.Pattern as Pattern
 import Kore.Internal.TermLike
-import Kore.Step.Simplification.AndTerms
-    ( termUnification
-    )
-import Kore.Step.Simplification.Data
-    ( runSimplifierBranch
-    )
-import qualified Kore.Step.Simplification.Not as Not
-import Kore.Unification.Error
-    ( UnificationError
-    )
-import Kore.Unification.UnifierT
-    ( runUnifierT
-    )
-import SMT
-    ( SMT
-    )
 
 import qualified Test.Kore.Builtin.Bool as Test.Bool
 import Test.Kore.Builtin.Builtin
@@ -80,38 +56,26 @@ test_KEqual =
         assertEqual' "" expect actual
 
     , testCaseWithSMT "kseq(x, dotk) equals kseq(x, dotk)" $ do
-        let expect = Pattern.top
+        let expect = Pattern.fromTermLike $ Test.Bool.asInternal True
             original =
-                mkEquals_
-                    (Test.Bool.asInternal True)
-                    (keqBool
-                        (kseq (mkElemVar (elemVarS "x" kItemSort)) dotk)
-                        (kseq (mkElemVar (elemVarS "x" kItemSort)) dotk)
+                keqBool
+                    (kseq
+                        (mkElemVar (elemVarS "x" kItemSort))
+                        dotk
                     )
-        actual <- evaluate original
-        assertEqual' "" expect actual
-
-    , testCaseWithSMT "kseq(inj(x), dotk) equals kseq(inj(x), dotk)" $ do
-        let expect = Pattern.top
-            original =
-                mkEquals_
-                    (Test.Bool.asInternal True)
-                    (keqBool
-                        (kseq (inj kItemSort (mkElemVar (elemVarS "x" idSort))) dotk)
-                        (kseq (inj kItemSort (mkElemVar (elemVarS "x" idSort))) dotk)
+                    (kseq
+                        (mkElemVar (elemVarS "x" kItemSort))
+                        dotk
                     )
         actual <- evaluate original
         assertEqual' "" expect actual
 
-    , testCaseWithSMT "distinct constructor-like terms" $ do
-        let expect = Pattern.top
+    , testCaseWithSMT "kseq(inj(x), dotk) equals kseq(inj(x), dotk)" $ do
+        let expect = Pattern.fromTermLike $ Test.Bool.asInternal True
             original =
-                mkEquals_
-                    (Test.Bool.asInternal False)
-                    (keqBool
-                        (kseq (inj kItemSort dvX) dotk)
-                        (kseq (inj kItemSort dvT) dotk)
-                    )
+                keqBool
+                    (kseq (inj kItemSort (mkElemVar (elemVarS "x" idSort))) dotk)
+                    (kseq (inj kItemSort (mkElemVar (elemVarS "x" idSort))) dotk)
         actual <- evaluate original
         assertEqual' "" expect actual
 
@@ -138,6 +102,17 @@ test_KEqual =
         actual <- evaluate original
         assertEqual' "" expect actual
     ]
+  where
+    dvT =
+        mkDomainValue DomainValue
+            { domainValueSort = idSort
+            , domainValueChild = mkStringLiteral "t"
+            }
+    dvX =
+        mkDomainValue DomainValue
+            { domainValueSort = idSort
+            , domainValueChild = mkStringLiteral "x"
+            }
 
 test_KIte :: [TestTree]
 test_KIte =
@@ -165,43 +140,3 @@ test_KIte =
         actual <- evaluate original
         assertEqual' "" expect actual
     ]
-
-test_KEqualSimplification :: [TestTree]
-test_KEqualSimplification =
-    [ testCaseWithSMT "constructor1 =/=K constructor2" $ do
-        let term1 = Test.Bool.asInternal False
-            term2 =
-                keqBool
-                    (kseq (inj kItemSort dvX) dotk)
-                    (kseq (inj kItemSort dvT) dotk)
-            expect = [Right [Just Pattern.top]]
-        actual <- runKEqualSimplification term1 term2
-        assertEqual' "" expect actual
-
-    ]
-
-dvT, dvX :: TermLike Variable
-dvT =
-    mkDomainValue DomainValue
-        { domainValueSort = idSort
-        , domainValueChild = mkStringLiteral "t"
-        }
-dvX =
-    mkDomainValue DomainValue
-        { domainValueSort = idSort
-        , domainValueChild = mkStringLiteral "x"
-        }
-
-runKEqualSimplification
-    :: TermLike Variable
-    -> TermLike Variable
-    -> SMT [Either UnificationError [Maybe (Pattern Variable)]]
-runKEqualSimplification term1 term2 =
-    runSimplifierBranch testEnv
-    . runUnifierT Not.notSimplifier
-    . runMaybeT
-    $ KEqual.termKEquals
-        (termUnification Not.notSimplifier)
-        Not.notSimplifier
-        term1
-        term2
diff --git a/test/not-kequal/Makefile b/test/itp-nth-ancestor/Makefile
similarity index 51%
rename from test/not-kequal/Makefile
rename to test/itp-nth-ancestor/Makefile
index 310e0746dd..ca9182299b 100644
--- a/test/not-kequal/Makefile
+++ b/test/itp-nth-ancestor/Makefile
@@ -1,3 +1,3 @@
-DEF := test
-MODULE := TEST
+DEF = chain
+KPROVE_MODULE = V
 include $(CURDIR)/../include.mk
diff --git a/test/itp-nth-ancestor/chain.k b/test/itp-nth-ancestor/chain.k
new file mode 100644
index 0000000000..f3c91cab37
--- /dev/null
+++ b/test/itp-nth-ancestor/chain.k
@@ -0,0 +1,86 @@
+/*
+    Coq-style proof of `ancestor_means`
+    https://github.com/runtimeverification/casper-proofs/blob/master/Core/AccountableSafety.v
+*/
+
+require "proof-script.k"
+
+module CHAIN-SYNTAX
+
+endmodule
+
+module CHAIN
+
+    imports PROOF-SCRIPT
+    imports CHAIN-SYNTAX
+
+    /*
+        (* abstract representation of a block tree *)
+        Variable hash_parent : rel Hash.
+
+        Notation "h1 <~ h2" := (hash_parent h1 h2) (at level 50).
+
+        Definition hash_ancestor h1 h2 :=
+         connect hash_parent h1 h2.
+
+        Notation "h1 <~* h2" := (hash_ancestor h1 h2) (at level 50).
+
+        Lemma hash_ancestor_base : forall h1 h2,
+          h1 <~ h2 -> h1 <~* h2.
+        Proof.
+        by apply/connect1.
+        Qed.
+
+        Lemma hash_ancestor_step : forall h1 h2 h3,
+         h1 <~ h2 -> h2 <~* h3 -> h1 <~* h3.
+        Proof.
+        move => h1 h2 h3.
+        move/connect1.
+        by apply/connect_trans.
+        Qed.
+    */
+
+    syntax Pred ::= Int "<~"  Int
+                  | Int "<~*" Int
+
+    rule
+    <k> apply("<~*.i") => . ... </k>
+    <g> B1 <~ B2 => B1 <~* B2 </g>
+
+    rule
+    <k> apply("<~*.i") => . ... </k>
+    <g> B1 <~ B2 and B2 <~* B3 => B1 <~* B3 </g>
+
+    /*
+        (* predicate stating first hash is ancestor of second hash at the indicated distance *)
+        Inductive nth_ancestor : nat -> Hash -> Hash -> Prop :=
+        | nth_ancestor_0 : forall h1, nth_ancestor 0 h1 h1
+        | nth_ancestor_nth : forall n h1 h2 h3,
+            nth_ancestor n h1 h2 -> h2 <~ h3 ->
+            nth_ancestor n.+1 h1 h3.
+    */
+
+    syntax Pred ::= nth(Int, Int, Int)
+                  | block(Int)
+                  | Int "==" Int
+
+    rule
+    <k> apply("nth.i") => . ... </k>
+    <g> block(B) => nth(0, B, B) </g>
+
+    rule
+    <k> apply("nth.i") => . ... </k>
+    <g> nth(N, B1, B2) and B2 <~ B3
+     => nth(N +Int 1, B1, B3) </g>
+
+    rule
+    <k> apply("nth.e") => . ... </k>
+    <g> nth(0, B1, B2) => B1 == B2 </g>
+
+    rule
+    <k> apply("nth.e") => . ... </k>
+    <g> nth(N, B1, B3)
+     => nth(N -Int 1, B1, ?B2:Int) and ?B2 <~ B3 </g>
+        requires N >Int 0
+
+endmodule
diff --git a/test/itp-nth-ancestor/nth1-spec.k b/test/itp-nth-ancestor/nth1-spec.k
new file mode 100644
index 0000000000..fb7e6bbb56
--- /dev/null
+++ b/test/itp-nth-ancestor/nth1-spec.k
@@ -0,0 +1,52 @@
+/*
+    Coq-style proof of `ancestor_means`
+    https://github.com/runtimeverification/casper-proofs/blob/master/Core/AccountableSafety.v
+*/
+/*
+    Lemma ancestor_means :
+      forall n parent new,
+      nth_ancestor n parent new -> n > 0 -> parent <~* new.
+    Proof.
+    elim => //=.
+    move => n IH parent new Hn.
+    inversion Hn; subst.
+    case Hn0: (n == 0).
+      move/eqP: Hn0 H0 -> => Hnt Hlt.
+      inversion Hnt; subst.
+      by apply/connect1.
+    move/negP/negP: Hn0 => Hn0 Hltn.
+    have Hnn: 0 < n.
+      apply: neq0_lt0n.
+      by apply/negP/negP.
+    move: (IH _ _ H0 Hnn) => Hp.
+    apply: connect_trans; eauto.
+    by apply/connect1.
+*/
+
+require "chain.k"
+
+// base case
+module NTH1-SPEC
+    imports V
+
+    rule
+    <g> nth(1, B1, B2) => B1 <~* B2 </g>
+    <p> .Map => ?_ </p>
+    <k> apply("nth.e")
+     ~> store2("p1", "p2")
+     ~> load("p1")
+     ~> apply("nth.e")
+     ~> load("p2")
+     ~> apply("lemma")
+     ~> apply("<~*.i")
+     => . </k>
+
+    rule
+    <k> apply("lemma") => . ... </k>
+    <g> B1 == B2 and B2 <~ B3 => B1 <~ B3 </g>
+        [trusted]
+endmodule
+
+module V
+    imports CHAIN
+endmodule
diff --git a/test/itp-nth-ancestor/nth1-spec.k.out.golden b/test/itp-nth-ancestor/nth1-spec.k.out.golden
new file mode 100644
index 0000000000..e663cb04e1
--- /dev/null
+++ b/test/itp-nth-ancestor/nth1-spec.k.out.golden
@@ -0,0 +1 @@
+#True
diff --git a/test/itp-nth-ancestor/nth2-spec.k b/test/itp-nth-ancestor/nth2-spec.k
new file mode 100644
index 0000000000..e60437d299
--- /dev/null
+++ b/test/itp-nth-ancestor/nth2-spec.k
@@ -0,0 +1,74 @@
+/*
+    Coq-style proof of `ancestor_means`
+    https://github.com/runtimeverification/casper-proofs/blob/master/Core/AccountableSafety.v
+*/
+/*
+    Lemma ancestor_means :
+      forall n parent new,
+      nth_ancestor n parent new -> n > 0 -> parent <~* new.
+    Proof.
+    elim => //=.
+    move => n IH parent new Hn.
+    inversion Hn; subst.
+    case Hn0: (n == 0).
+      move/eqP: Hn0 H0 -> => Hnt Hlt.
+      inversion Hnt; subst.
+      by apply/connect1.
+    move/negP/negP: Hn0 => Hn0 Hltn.
+    have Hnn: 0 < n.
+      apply: neq0_lt0n.
+      by apply/negP/negP.
+    move: (IH _ _ H0 Hnn) => Hp.
+    apply: connect_trans; eauto.
+    by apply/connect1.
+*/
+
+require "chain.k"
+
+// inductive case
+module NTH2-SPEC
+    imports V
+
+    rule
+    <g> nth(k(N) +Int 1, B1, B2) => B1 <~* B2 </g>
+    <p> .Map => ?_ </p>
+    <k> apply("nth.e")
+     ~> store2("p1", "p2")
+     ~> load("p1")
+     ~> apply("ih")
+     ~> load("p2")
+     ~> apply("lemma")
+     => . </k>
+        requires k(N) >Int 0 andBool const(N)
+
+    // induction hypothesis
+    rule
+    <k> apply("ih") => . ... </k>
+    <g> nth(k(N), B1, B2) => B1 <~* B2 </g>
+        requires k(N) >Int 0 andBool const(N)
+        [trusted]
+
+    /*
+        Lemma hash_ancestor_intro' :
+          forall h1 h2 h3, h1 <~* h2 -> h2 <~ h3 -> h1 <~* h3.
+        Proof.
+        move => h1 h2 h3 H1 H2.
+        apply: connect_trans; eauto.
+        by apply/connect1.
+        Qed.
+    */
+    rule
+    <k> apply("lemma") => . ... </k>
+    <g> B1 <~* B2 and B2 <~ B3 => B1 <~* B3 </g>
+        [trusted]
+endmodule
+
+module V
+    imports CHAIN
+
+    syntax Bool ::= const(Int) [function, smtlib(con)]
+
+    syntax Int ::= k(Int) [function, functional, injective, smtlib(k)]
+
+    rule (k(N) +Int 1) -Int 1 => k(N)
+endmodule
diff --git a/test/itp-nth-ancestor/nth2-spec.k.out.golden b/test/itp-nth-ancestor/nth2-spec.k.out.golden
new file mode 100644
index 0000000000..e663cb04e1
--- /dev/null
+++ b/test/itp-nth-ancestor/nth2-spec.k.out.golden
@@ -0,0 +1 @@
+#True
diff --git a/test/itp-nth-ancestor/proof-script.k b/test/itp-nth-ancestor/proof-script.k
new file mode 100644
index 0000000000..7bfa88a083
--- /dev/null
+++ b/test/itp-nth-ancestor/proof-script.k
@@ -0,0 +1,42 @@
+// K ITP proof script language
+
+module PROOF-SCRIPT
+
+    imports STRING
+    imports MAP
+
+    configuration <T>
+      <k> $PGM:Script </k>
+      <g> .K </g> // workspace
+      <p> .Map </p> // premises
+    </T>
+
+    syntax Pred ::= Pred "and" Pred
+                  | "none"
+                  | Bool
+
+    syntax Script ::= apply(String)
+                    | load(String)
+                    | store1(String)
+                    | store2(String, String)
+
+    rule [load]:
+    <k> load(N) => . ... </k>
+    <g> X => #if X ==K none
+             #then         M [ N ]
+             #else X and { M [ N ] }:>Pred
+             #fi </g>
+    <p> M </p>
+
+    rule [store1]:
+    <k> store1(N) => . ... </k>
+    <g> X => none </g>
+    <p> M => M [ N <- X ] </p>
+
+    rule [store2]:
+    <k> store2(N1,N2) => . ... </k>
+    <g> X1 and X2 => none </g>
+    <p> M => M [ N1 <- X1 ]
+               [ N2 <- X2 ] </p>
+
+endmodule
diff --git a/test/not-kequal/a.test b/test/not-kequal/a.test
deleted file mode 100644
index 5c63345a42..0000000000
--- a/test/not-kequal/a.test
+++ /dev/null
@@ -1 +0,0 @@
-#changesState(b,123)
diff --git a/test/not-kequal/a.test.out.golden b/test/not-kequal/a.test.out.golden
deleted file mode 100644
index 937a92cf66..0000000000
--- a/test/not-kequal/a.test.out.golden
+++ /dev/null
@@ -1,3 +0,0 @@
-<k>
-  true
-</k>
diff --git a/test/not-kequal/test.k b/test/not-kequal/test.k
deleted file mode 100644
index 2671411cf5..0000000000
--- a/test/not-kequal/test.k
+++ /dev/null
@@ -1,15 +0,0 @@
-module TEST
-  imports BOOL
-  imports INT
-
-  syntax OpCode ::= "a" | "b" | "c" | "d" | "e" | "f" | "g"
-
-  syntax Bool ::= #changesState(OpCode, Int) [function]
-
-  rule #changesState(a, VALUE) => VALUE =/=Int 0
-  rule #changesState(OP,    _) => ( OP ==K b
-                                  orBool OP ==K c
-                                  )
-    requires notBool ( OP ==K a )
-
-endmodule