content: -----------------------------------------------------------------------------
  -- |
  -- Module    : Data.SBV.TP.List
  -- Copyright : (c) Levent Erkok
  -- License   : BSD3
  -- Maintainer: erkokl@gmail.com
  -- Stability : experimental
  --
  -- A variety of TP proofs on list processing functions. Note that
  -- these proofs only hold for finite lists. SMT-solvers do not model infinite
  -- lists, and hence all claims are for finite (but arbitrary-length) lists.
  -----------------------------------------------------------------------------
  
  {-# LANGUAGE CPP                 #-}
  {-# LANGUAGE DataKinds           #-}
  {-# LANGUAGE OverloadedLists     #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE QuasiQuotes         #-}
  {-# LANGUAGE TypeAbstractions    #-}
  {-# LANGUAGE TypeApplications    #-}
  
  {-# OPTIONS_GHC -Wall -Werror #-}
  
  module Data.SBV.TP.List (
       -- * Append
       appendNull, consApp, appendAssoc, initsLength, tailsLength, tailsAppend
  
       -- * Reverse
     , revLen, revApp, revCons, revSnoc, revRev, enumLen, revNM
  
       -- * Length
     , lengthTail, lenAppend, lenAppend2
  
       -- * Replicate
     , replicateLength
  
       -- * All and any
     , allAny
  
       -- * Map
     , mapEquiv, mapAppend, mapReverse, mapCompose
  
       -- * Foldr and foldl
     , foldrMapFusion, foldrFusion, foldrOverAppend, foldlOverAppend, foldrFoldlDuality, foldrFoldlDualityGeneralized, foldrFoldl
     , bookKeeping
  
       -- * Filter
     , filterAppend, filterConcat, takeDropWhile
  
       -- * Stutter removal
     , destutter, destutterIdempotent
  
       -- * Difference
     , appendDiff, diffAppend, diffDiff
  
       -- * Partition
     , partition1, partition2
  
      -- * Take and drop
     , take_take, drop_drop, take_drop, take_cons, take_map, drop_cons, drop_map, length_take, length_drop, take_all, drop_all
     , take_append, drop_append
  
     -- * Zip
     , map_fst_zip
     , map_snd_zip
     , map_fst_zip_take
     , map_snd_zip_take
  
     -- * Counting elements
     , count, countAppend, takeDropCount, countNonNeg, countElem, elemCount
  
     -- * Disjointness
     , disjoint, disjointDiff
  
     -- * Interleaving
     , interleave, uninterleave, interleaveLen, interleaveRoundTrip
   ) where
  
  import Prelude (Integer, Bool, Eq, ($), Num(..), id, (.), flip)
  
  import Data.SBV
  import Data.SBV.List
  import Data.SBV.Tuple
  import Data.SBV.TP
  
  #ifdef DOCTEST
  -- $setup
  -- >>> :set -XScopedTypeVariables
  -- >>> :set -XTypeApplications
  -- >>> import Data.SBV
  -- >>> import Data.SBV.TP
  -- >>> import Control.Exception
  #endif
  
  -- | @xs ++ [] == xs@
  --
  -- >>> runTP $ appendNull @Integer
  -- Lemma: appendNull                       Q.E.D.
  -- [Proven] appendNull :: Ɐxs ∷ [Integer] → Bool
  appendNull :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool))
  appendNull = lemma "appendNull"
                     (\(Forall xs) -> xs ++ nil .== xs)
                     []
  
  -- | @(x : xs) ++ ys == x : (xs ++ ys)@
  --
  -- >>> runTP $ consApp @Integer
  -- Lemma: consApp                          Q.E.D.
  -- [Proven] consApp :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
  consApp :: forall a. SymVal a => TP (Proof (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))
  consApp = lemma "consApp"
                  (\(Forall x) (Forall xs) (Forall ys) -> (x .: xs) ++ ys .== x .: (xs ++ ys))
                  []
  
  -- | @(xs ++ ys) ++ zs == xs ++ (ys ++ zs)@
  --
  -- >>> runTP $ appendAssoc @Integer
  -- Lemma: appendAssoc                      Q.E.D.
  -- [Proven] appendAssoc :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Ɐzs ∷ [Integer] → Bool
  --
  -- Surprisingly, z3 can prove this without any induction. (Since SBV's append translates directly to
  -- the concatenation of sequences in SMTLib, it must trigger an internal heuristic in z3
  -- that proves it right out-of-the-box!)
  appendAssoc :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> Forall "zs" [a] -> SBool))
  appendAssoc =
     lemma "appendAssoc"
           (\(Forall xs) (Forall ys) (Forall zs) -> xs ++ (ys ++ zs) .== (xs ++ ys) ++ zs)
           []
  
  -- | @length (inits xs) == 1 + length xs@
  --
  -- >>> runTP $ initsLength @Integer
  -- Inductive lemma (strong): initsLength
  --   Step: Measure is non-negative         Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] initsLength :: Ɐxs ∷ [Integer] → Bool
  initsLength :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool))
  initsLength =
     sInduct "initsLength"
             (\(Forall xs) -> length (inits xs) .== 1 + length xs)
             (length @a) $
             \ih xs -> [] |- length (inits xs)
                          ?? ih
                          =: 1 + length xs
                          =: qed
  
  -- | @length (tails xs) == 1 + length xs@
  --
  -- >>> runTP $ tailsLength @Integer
  -- Inductive lemma: tailsLength
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] tailsLength :: Ɐxs ∷ [Integer] → Bool
  tailsLength :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool))
  tailsLength =
     induct "tailsLength"
            (\(Forall xs) -> length (tails xs) .== 1 + length xs) $
            \ih (x, xs) -> [] |- length (tails (x .: xs))
                              =: length (tails xs ++ [x .: xs])
                              =: length (tails xs) + 1
                              ?? ih
                              =: 1 + length xs + 1
                              =: 1 + length (x .: xs)
                              =: qed
  
  -- | @tails (xs ++ ys) == map (++ ys) (tails xs) ++ tail (tails ys)@
  --
  -- This property comes from Richard Bird's "Pearls of functional Algorithm Design" book, chapter 2.
  -- Note that it is not exactly as stated there, as the definition of @tail@ Bird uses is different
  -- than the standard Haskell function @tails@: Bird's version does not return the empty list as the
  -- tail. So, we slightly modify it to fit the standard definition. (NB. z3 is finicky on this
  -- problem, while cvc5 works much better.)
  --
  -- >>> runTPWith cvc5 $ tailsAppend @Integer
  -- Inductive lemma: base case
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: helper
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Inductive lemma: tailsAppend
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] tailsAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
  tailsAppend :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
  tailsAppend = do
  
     let -- Ideally, we would like to define appendEach like this:
         --
         --       appendEach xs ys = map (++ ys) xs
         --
         -- But capture of ys is not allowed when we use the higher-order
         -- function map in SBV. So, we create a closure instead.
         appendEach :: SList a -> SList [a] -> SList [a]
         appendEach ys = map $ Closure { closureEnv = ys
                                       , closureFun = \env xs -> xs ++ env
                                       }
  
     -- Even proving the base case of induction is hard due to recursive definition. So we first prove the base case by induction.
     bc <- induct "base case"
                  (\(Forall @"ys" (ys :: SList a)) -> tails ys .== [ys] ++ tail (tails ys)) $
                  \ih (y, ys) -> [] |- tails (y .: ys)
                                    =: [y .: ys] ++ tails ys
                                    ?? ih
                                    =: [y .: ys] ++ [ys] ++ tail (tails ys)
                                    =: [y .: ys] ++ tail (tails (y .: ys))
                                    =: qed
  
     -- Also need a helper to relate how appendEach and tails work together
     helper <- calc "helper"
                     (\(Forall @"xs" xs) (Forall @"ys" ys) (Forall @"x" x) ->
                          appendEach ys (tails (x .: xs)) .== [(x .: xs) ++ ys] ++ appendEach ys (tails xs)) $
                     \xs ys x -> [] |- appendEach ys (tails (x .: xs))
                                    =: appendEach ys ([x .: xs] ++ tails xs)
                                    =: [(x .: xs) ++ ys] ++ appendEach ys (tails xs)
                                    =: qed
  
     induct "tailsAppend"
            (\(Forall xs) (Forall ys) -> tails (xs ++ ys) .== appendEach ys (tails xs) ++ tail (tails ys)) $
            \ih (x, xs) ys -> [assumptionFromProof bc]
                           |- tails ((x .: xs) ++ ys)
                           =: tails (x .: (xs ++ ys))
                           =: [x .: (xs ++ ys)] ++ tails (xs ++ ys)
                           ?? ih
                           =: [(x .: xs) ++ ys] ++ appendEach ys (tails xs) ++ tail (tails ys)
                           ?? helper
                           =: appendEach ys (tails (x .: xs)) ++ tail (tails ys)
                           =: qed
  
  -- | @length xs == length (reverse xs)@
  --
  -- >>> runTP $ revLen @Integer
  -- Inductive lemma: revLen
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] revLen :: Ɐxs ∷ [Integer] → Bool
  revLen :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool))
  revLen = induct "revLen"
                  (\(Forall xs) -> length (reverse xs) .== length xs) $
                  \ih (x, xs) -> [] |- length (reverse (x .: xs))
                                    =: length (reverse xs ++ [x])
                                    =: length (reverse xs) + length [x]
                                    ?? ih
                                    =: length xs + 1
                                    =: length (x .: xs)
                                    =: qed
  
  -- | @reverse (xs ++ ys) .== reverse ys ++ reverse xs@
  --
  -- >>> runTP $ revApp @Integer
  -- Inductive lemma: revApp
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] revApp :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
  revApp :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
  revApp = induct "revApp"
                   (\(Forall xs) (Forall ys) -> reverse (xs ++ ys) .== reverse ys ++ reverse xs) $
                   \ih (x, xs) ys -> [] |- reverse ((x .: xs) ++ ys)
                                        =: reverse (x .: (xs ++ ys))
                                        =: reverse (xs ++ ys) ++ [x]
                                        ?? ih
                                        =: (reverse ys ++ reverse xs) ++ [x]
                                        =: reverse ys ++ (reverse xs ++ [x])
                                        =: reverse ys ++ reverse (x .: xs)
                                        =: qed
  
  -- | @reverse (x:xs) == reverse xs ++ [x]@
  --
  -- >>> runTP $ revCons @Integer
  -- Lemma: revCons                          Q.E.D.
  -- [Proven] revCons :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool
  revCons :: forall a. SymVal a => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))
  revCons = lemma "revCons"
                  (\(Forall x) (Forall xs) -> reverse (x .: xs) .== reverse xs ++ [x])
                  []
  
  -- | @reverse (xs ++ [x]) == x : reverse xs@
  --
  -- >>> runTP $ revSnoc @Integer
  -- Inductive lemma: revApp
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: revSnoc                          Q.E.D.
  -- [Proven] revSnoc :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool
  revSnoc :: forall a. SymVal a => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))
  revSnoc = do
     ra <- revApp @a
  
     lemma "revSnoc"
           (\(Forall x) (Forall xs) -> reverse (xs ++ [x]) .== x .: reverse xs)
           [proofOf ra]
  
  -- | @reverse (reverse xs) == xs@
  --
  -- >>> runTP $ revRev @Integer
  -- Inductive lemma: revApp
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Inductive lemma: revRev
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] revRev :: Ɐxs ∷ [Integer] → Bool
  revRev :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool))
  revRev = do
  
     ra <- revApp @a
  
     induct "revRev"
            (\(Forall xs) -> reverse (reverse xs) .== xs) $
            \ih (x, xs) -> [] |- reverse (reverse (x .: xs))
                              =: reverse (reverse xs ++ [x])
                              ?? ra
                              =: reverse [x] ++ reverse (reverse xs)
                              ?? ih
                              =: [x] ++ xs
                              =: x .: xs
                              =: qed
  
  -- | \(\text{length } [n \dots m] = \max(0,\; m - n + 1)\)
  --
  -- The proof uses the metric @|m-n|@.
  --
  -- >>> runTP enumLen
  -- Inductive lemma (strong): enumLen
  --   Step: Measure is non-negative         Q.E.D.
  --   Step: 1 (2 way case split)
  --     Step: 1.1                           Q.E.D.
  --     Step: 1.2.1                         Q.E.D.
  --     Step: 1.2.2                         Q.E.D.
  --     Step: 1.2.3                         Q.E.D.
  --     Step: 1.2.4                         Q.E.D.
  --     Step: 1.Completeness                Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] enumLen :: Ɐn ∷ Integer → Ɐm ∷ Integer → Bool
  enumLen :: TP (Proof (Forall "n" Integer -> Forall "m" Integer -> SBool))
  enumLen =
    sInduct "enumLen"
            (\(Forall n) (Forall m) -> length [sEnum|n .. m|] .== 0 `smax` (m - n + 1))
            (\n m -> abs (m - n)) $
            \ih n m -> [] |- length [sEnum|n+1 .. m|]
                          =: cases [ n+1 .>  m ==> trivial
                                   , n+1 .<= m ==> length (n+1 .: [sEnum|n+2 .. m|])
                                                =: 1 + length [sEnum|n+2 .. m|]
                                                ?? ih
                                                =: 1 + (0 `smax` (m - (n+2) + 1))
                                                =: 0 `smax` (m - (n+1) + 1)
                                                =: qed
                                   ]
  
  -- | @reverse [n .. m] == [m, m-1 .. n]@
  --
  -- The proof uses the metric @|m-n|@.
  --
  -- >>> runTP $ revNM
  -- Inductive lemma (strong): helper
  --   Step: Measure is non-negative         Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Inductive lemma (strong): revNM
  --   Step: Measure is non-negative         Q.E.D.
  --   Step: 1 (2 way case split)
  --     Step: 1.1                           Q.E.D.
  --     Step: 1.2.1                         Q.E.D.
  --     Step: 1.2.2                         Q.E.D.
  --     Step: 1.2.3                         Q.E.D.
  --     Step: 1.2.4                         Q.E.D.
  --     Step: 1.Completeness                Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] revNM :: Ɐn ∷ Integer → Ɐm ∷ Integer → Bool
  revNM :: TP (Proof (Forall "n" Integer -> Forall "m" Integer -> SBool))
  revNM = do
  
    helper <- sInduct "helper"
                      (\(Forall @"m" (m :: SInteger)) (Forall @"n" n) ->
                            n .< m .=> [sEnum|m, m-1 .. n+1|] ++ [n] .== [sEnum|m, m-1 .. n|])
                      (\m n -> abs (m - n)) $
                      \ih m n -> [n .< m] |- [sEnum|m, m-1 .. n+1|] ++ [n]
                                          =: m .: [sEnum|m-1, m-2 .. n+1|] ++ [n]
                                          ?? ih
                                          =: m .: [sEnum|m-1, m-2 .. n|]
                                          =: [sEnum|m, m-1 .. n|]
                                          =: qed
  
    sInduct "revNM"
            (\(Forall n) (Forall m) -> reverse [sEnum|n .. m|] .== [sEnum|m, m-1 .. n|])
            (\n m -> abs (m - n)) $
            \ih n m -> [] |- reverse [sEnum|n .. m|]
                          =: cases [ n .>  m ==> trivial
                                   , n .<= m ==> reverse (n .: [sEnum|(n+1) .. m|])
                                              =: reverse [sEnum|(n+1) .. m|] ++ [n]
                                              ?? ih
                                              =: [sEnum|m, m-1 .. n+1|] ++ [n]
                                              ?? helper
                                              =: [sEnum|m, m-1 .. n|]
                                              =: qed
                                   ]
  
  -- | @length (x : xs) == 1 + length xs@
  --
  -- >>> runTP $ lengthTail @Integer
  -- Lemma: lengthTail                       Q.E.D.
  -- [Proven] lengthTail :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool
  lengthTail :: forall a. SymVal a => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))
  lengthTail = lemma "lengthTail"
                     (\(Forall x) (Forall xs) -> length (x .: xs) .== 1 + length xs)
                     []
  
  -- | @length (xs ++ ys) == length xs + length ys@
  --
  -- >>> runTP $ lenAppend @Integer
  -- Lemma: lenAppend                        Q.E.D.
  -- [Proven] lenAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
  lenAppend :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
  lenAppend = lemma "lenAppend"
                    (\(Forall xs) (Forall ys) -> length (xs ++ ys) .== length xs + length ys)
                    []
  
  -- | @length xs == length ys -> length (xs ++ ys) == 2 * length xs@
  --
  -- >>> runTP $ lenAppend2 @Integer
  -- Lemma: lenAppend2                       Q.E.D.
  -- [Proven] lenAppend2 :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
  lenAppend2 :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
  lenAppend2 = lemma "lenAppend2"
                     (\(Forall xs) (Forall ys) -> length xs .== length ys .=> length (xs ++ ys) .== 2 * length xs)
                     []
  
  -- | @length (replicate k x) == max (0, k)@
  --
  -- >>> runTP $ replicateLength @Integer
  -- Inductive lemma: replicateLength
  --   Step: Base                            Q.E.D.
  --   Step: 1 (2 way case split)
  --     Step: 1.1                           Q.E.D.
  --     Step: 1.2.1                         Q.E.D.
  --     Step: 1.2.2                         Q.E.D.
  --     Step: 1.2.3                         Q.E.D.
  --     Step: 1.2.4                         Q.E.D.
  --     Step: 1.Completeness                Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] replicateLength :: Ɐk ∷ Integer → Ɐx ∷ Integer → Bool
  replicateLength :: forall a. SymVal a => TP (Proof (Forall "k" Integer -> Forall "x" a -> SBool))
  replicateLength = induct "replicateLength"
                           (\(Forall k) (Forall x) -> length (replicate k x) .== 0 `smax` k) $
                           \ih k x -> [] |- length (replicate (k+1) x)
                                         =: cases [ k .< 0  ==> trivial
                                                  , k .>= 0 ==> length (x .: replicate k x)
                                                             =: 1 + length (replicate k x)
                                                             ?? ih
                                                             =: 1 + 0 `smax` k
                                                             =: 0 `smax` (k+1)
                                                             =: qed
                                                  ]
  
  -- | @not (all id xs) == any not xs@
  --
  -- A list of booleans is not all true, if any of them is false.
  --
  -- >>> runTP allAny
  -- Inductive lemma: allAny
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] allAny :: Ɐxs ∷ [Bool] → Bool
  allAny :: TP (Proof (Forall "xs" [Bool] -> SBool))
  allAny = induct "allAny"
                  (\(Forall xs) -> sNot (all id xs) .== any sNot xs) $
                  \ih (x, xs) -> [] |- sNot (all id (x .: xs))
                                    =: sNot (x .&& all id xs)
                                    =: (sNot x .|| sNot (all id xs))
                                    ?? ih
                                    =: sNot x .|| any sNot xs
                                    =: any sNot (x .: xs)
                                    =: qed
  
  -- | @f == g ==> map f xs == map g xs@
  --
  -- >>> runTP $ mapEquiv @Integer @Integer (uninterpret "f") (uninterpret "g")
  -- Inductive lemma: mapEquiv
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] mapEquiv :: Ɐxs ∷ [Integer] → Bool
  mapEquiv :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b) -> (SBV a -> SBV b) -> TP (Proof (Forall "xs" [a] -> SBool))
  mapEquiv f g = do
     let f'eq'g :: SBool
         f'eq'g = quantifiedBool $ \(Forall x) -> f x .== g x
  
     induct "mapEquiv"
            (\(Forall xs) -> f'eq'g .=> map f xs .== map g xs) $
            \ih (x, xs) -> [f'eq'g] |- map f (x .: xs) .== map g (x .: xs)
                                    =: f x .: map f xs .== g x .: map g xs
                                    =: f x .: map f xs .== f x .: map g xs
                                    ?? ih
                                    =: f x .: map f xs .== f x .: map f xs
                                    =: map f (x .: xs) .== map f (x .: xs)
                                    =: qed
  
  -- | @map f (xs ++ ys) == map f xs ++ map f ys@
  --
  -- >>> runTP $ mapAppend @Integer @Integer (uninterpret "f")
  -- Inductive lemma: mapAppend
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] mapAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
  mapAppend :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b) -> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
  mapAppend f =
     induct "mapAppend"
            (\(Forall xs) (Forall ys) -> map f (xs ++ ys) .== map f xs ++ map f ys) $
            \ih (x, xs) ys -> [] |- map f ((x .: xs) ++ ys)
                                 =: map f (x .: (xs ++ ys))
                               =: f x .: map f (xs ++ ys)
                               ?? ih
                               =: f x .: (map f xs  ++ map f ys)
                               =: (f x .: map f xs) ++ map f ys
                               =: map f (x .: xs) ++ map f ys
                               =: qed
  
  -- | @map f . reverse == reverse . map f@
  --
  -- >>> runTP $ mapReverse @Integer @String (uninterpret "f")
  -- Inductive lemma: mapAppend
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Inductive lemma: mapReverse
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Step: 6                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] mapReverse :: Ɐxs ∷ [Integer] → Bool
  mapReverse :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b) -> TP (Proof (Forall "xs" [a] -> SBool))
  mapReverse f = do
       mApp <- mapAppend f
  
       induct "mapReverse"
              (\(Forall xs) -> reverse (map f xs) .== map f (reverse xs)) $
              \ih (x, xs) -> [] |- reverse (map f (x .: xs))
                                =: reverse (f x .: map f xs)
                                =: reverse (map f xs) ++ [f x]
                                ?? ih
                                =: map f (reverse xs) ++ [f x]
                                =: map f (reverse xs) ++ map f [x]
                                ?? mApp
                                =: map f (reverse xs ++ [x])
                                =: map f (reverse (x .: xs))
                                =: qed
  
  -- | @map f . map g == map (f . g)@
  --
  -- >>> runTP $ mapCompose @Integer @Bool @String (uninterpret "f") (uninterpret "g")
  -- Inductive lemma: mapCompose
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] mapCompose :: Ɐxs ∷ [Integer] → Bool
  mapCompose :: forall a b c. (SymVal a, SymVal b, SymVal c) => (SBV a -> SBV b) -> (SBV b -> SBV c) -> TP (Proof (Forall "xs" [a] -> SBool))
  mapCompose f g =
    induct "mapCompose"
           (\(Forall xs) -> map g (map f xs) .== map (g . f) xs) $
           \ih (x, xs) -> [] |- map g (map f (x .: xs))
                             =: map g (f x .: map f xs)
                             =: g (f x) .: map g (map f xs)
                             ?? ih
                             =: g (f x) .: map (g . f) xs
                             =: (g . f) x .: map (g . f) xs
                             =: map (g . f) (x .: xs)
                             =: qed
  
  -- | @foldr f a . map g == foldr (f . g) a@
  --
  -- >>> runTP $ foldrMapFusion @String @Bool @Integer (uninterpret "a") (uninterpret "b") (uninterpret "c")
  -- Inductive lemma: foldrMapFusion
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] foldrMapFusion :: Ɐxs ∷ [[Char]] → Bool
  foldrMapFusion :: forall a b c. (SymVal a, SymVal b, SymVal c) => SBV c -> (SBV a -> SBV b) -> (SBV b -> SBV c -> SBV c) -> TP (Proof (Forall "xs" [a] -> SBool))
  foldrMapFusion a g f =
    induct "foldrMapFusion"
           (\(Forall xs) -> foldr f a (map g xs) .== foldr (f . g) a xs) $
           \ih (x, xs) -> [] |- foldr f a (map g (x .: xs))
                             =: foldr f a (g x .: map g xs)
                             =: g x `f` foldr f a (map g xs)
                             ?? ih
                             =: g x `f` foldr (f . g) a xs
                             =: foldr (f . g) a (x .: xs)
                             =: qed
  
  -- |
  --
  -- @
  --   f . foldr g a == foldr h b
  --   provided, f a = b and for all x and y, f (g x y) == h x (f y).
  -- @
  --
  -- >>> runTP $ foldrFusion @String @Bool @Integer (uninterpret "a") (uninterpret "b") (uninterpret "f") (uninterpret "g") (uninterpret "h")
  -- Inductive lemma: foldrFusion
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] foldrFusion :: Ɐxs ∷ [[Char]] → Bool
  foldrFusion :: forall a b c. (SymVal a, SymVal b, SymVal c) => SBV c -> SBV b -> (SBV c -> SBV b) -> (SBV a -> SBV c -> SBV c) -> (SBV a -> SBV b -> SBV b) -> TP (Proof (Forall "xs" [a] -> SBool))
  foldrFusion a b f g h = do
     let -- Assumptions under which the equality holds
         h1 = f a .== b
         h2 = quantifiedBool $ \(Forall x) (Forall y) -> f (g x y) .== h x (f y)
  
     induct "foldrFusion"
            (\(Forall xs) -> h1 .&& h2 .=> f (foldr g a xs) .== foldr h b xs) $
            \ih (x, xs) -> [h1, h2] |- f (foldr g a (x .: xs))
                                    =: f (g x (foldr g a xs))
                                    =: h x (f (foldr g a xs))
                                    ?? ih
                                    =: h x (foldr h b xs)
                                    =: foldr h b (x .: xs)
                                    =: qed
  
  -- | @foldr f a (xs ++ ys) == foldr f (foldr f a ys) xs@
  --
  -- >>> runTP $ foldrOverAppend @Integer (uninterpret "a") (uninterpret "f")
  -- Inductive lemma: foldrOverAppend
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] foldrOverAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
  foldrOverAppend :: forall a. SymVal a => SBV a -> (SBV a -> SBV a -> SBV a) -> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
  foldrOverAppend a f =
     induct "foldrOverAppend"
            (\(Forall xs) (Forall ys) -> foldr f a (xs ++ ys) .== foldr f (foldr f a ys) xs) $
            \ih (x, xs) ys -> [] |- foldr f a ((x .: xs) ++ ys)
                                 =: foldr f a (x .: (xs ++ ys))
                                 =: x `f` foldr f a (xs ++ ys)
                                 ?? ih
                                 =: x `f` foldr f (foldr f a ys) xs
                                 =: foldr f (foldr f a ys) (x .: xs)
                                 =: qed
  
  -- | @foldl f e (xs ++ ys) == foldl f (foldl f e xs) ys@
  --
  -- >>> runTP $ foldlOverAppend @Integer @Bool (uninterpret "f")
  -- Inductive lemma: foldlOverAppend
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] foldlOverAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Ɐe ∷ Bool → Bool
  foldlOverAppend :: forall a b. (SymVal a, SymVal b) => (SBV b -> SBV a -> SBV b) -> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" b -> SBool))
  foldlOverAppend f =
     induct "foldlOverAppend"
            (\(Forall xs) (Forall ys) (Forall a) -> foldl f a (xs ++ ys) .== foldl f (foldl f a xs) ys) $
            \ih (x, xs) ys a -> [] |- foldl f a ((x .: xs) ++ ys)
                                   =: foldl f a (x .: (xs ++ ys))
                                   =: foldl f (a `f` x) (xs ++ ys)
                                   -- z3 is smart enough to instantiate the IH correctly below, but we're
                                   -- using an explicit instantiation to be clear about the use of @a@ at a different value
                                   ?? ih `at` (Inst @"ys" ys, Inst @"e" (a `f` x))
                                   =: foldl f (foldl f (a `f` x) xs) ys
                                   =: qed
  
  -- | @foldr f e xs == foldl (flip f) e (reverse xs)@
  --
  -- >>> runTP $ foldrFoldlDuality @Integer @String (uninterpret "f")
  -- Inductive lemma: foldlOverAppend
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Inductive lemma: foldrFoldlDuality
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Step: 6                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] foldrFoldlDuality :: Ɐxs ∷ [Integer] → Ɐe ∷ [Char] → Bool
  foldrFoldlDuality :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b -> SBV b) -> TP (Proof (Forall "xs" [a] -> Forall "e" b -> SBool))
  foldrFoldlDuality f = do
     foa <- foldlOverAppend (flip f)
  
     induct "foldrFoldlDuality"
            (\(Forall xs) (Forall e) -> foldr f e xs .== foldl (flip f) e (reverse xs)) $
            \ih (x, xs) e -> [] |- let ff  = flip f
                                       rxs = reverse xs
                                   in foldr f e (x .: xs)
                                   =: x `f` foldr f e xs
                                   ?? ih
                                   =: x `f` foldl ff e rxs
                                   =: foldl ff e rxs `ff` x
                                   =: foldl ff (foldl ff e rxs) [x]
                                   ?? foa
                                   =: foldl ff e (rxs ++ [x])
                                   =: foldl ff e (reverse (x .: xs))
                                   =: qed
  
  -- | Given:
  --
  -- @
  --     x \@ (y \@ z) = (x \@ y) \@ z     (associativity of @)
  -- and e \@ x = x                     (left unit)
  -- and x \@ e = x                     (right unit)
  -- @
  --
  -- Proves:
  --
  -- @
  --     foldr (\@) e xs == foldl (\@) e xs
  -- @
  --
  -- >>> runTP $ foldrFoldlDualityGeneralized @Integer (uninterpret "e") (uninterpret "|@|")
  -- Inductive lemma: helper
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Inductive lemma: foldrFoldlDuality
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Step: 6                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] foldrFoldlDuality :: Ɐxs ∷ [Integer] → Bool
  foldrFoldlDualityGeneralized :: forall a. SymVal a => SBV a -> (SBV a -> SBV a -> SBV a) -> TP (Proof (Forall "xs" [a] -> SBool))
  foldrFoldlDualityGeneralized e (@) = do
     -- Assumptions under which the equality holds
     let assoc = quantifiedBool $ \(Forall x) (Forall y) (Forall z) -> x @ (y @ z) .== (x @ y) @ z
         lunit = quantifiedBool $ \(Forall x) -> e @ x .== x
         runit = quantifiedBool $ \(Forall x) -> x @ e .== x
  
     -- Helper: foldl (@) (y @ z) xs = y @ foldl (@) z xs
     -- Note the instantiation of the IH at a different value for z. It turns out
     -- we don't have to actually specify this since z3 can figure it out by itself, but we're being explicit.
     helper <- induct "helper"
                      (\(Forall @"xs" xs) (Forall @"y" y) (Forall @"z" z) -> assoc .=> foldl (@) (y @ z) xs .== y @ foldl (@) z xs) $
                      \ih (x, xs) y z -> [assoc] |- foldl (@) (y @ z) (x .: xs)
                                                 =: foldl (@) ((y @ z) @ x) xs
                                                 ?? assoc
                                                 =: foldl (@) (y @ (z @ x)) xs
                                                 ?? ih `at` (Inst @"y" y, Inst @"z" (z @ x))
                                                 =: y @ foldl (@) (z @ x) xs
                                                 =: y @ foldl (@) z (x .: xs)
                                                 =: qed
  
     induct "foldrFoldlDuality"
            (\(Forall xs) -> assoc .&& lunit .&& runit .=> foldr (@) e xs .== foldl (@) e xs) $
            \ih (x, xs) -> [assoc, lunit, runit] |- foldr (@) e (x .: xs)
                                                 =: x @ foldr (@) e xs
                                                 ?? ih
                                                 =: x @ foldl (@) e xs
                                                 ?? helper
                                                 =: foldl (@) (x @ e) xs
                                                 ?? runit
                                                 =: foldl (@) x xs
                                                 ?? lunit
                                                 =: foldl (@) (e @ x) xs
                                                 =: foldl (@) e (x .: xs)
                                                 =: qed
  
  -- | Given:
  --
  -- @
  --        (x \<+> y) \<*> z = x \<+> (y \<*> z)
  --   and  x \<+> e = e \<*> x
  -- @
  --
  -- Proves:
  --
  -- @
  --    foldr (\<+>) e xs = foldl (\<*>) e xs
  -- @
  --
  -- In Bird's Introduction to Functional Programming book (2nd edition) this is called the second duality theorem:
  --
  -- >>> runTP $ foldrFoldl @Integer @String (uninterpret "<+>") (uninterpret "<*>") (uninterpret "e")
  -- Inductive lemma: foldl over <*>/<+>
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Inductive lemma: foldrFoldl
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] foldrFoldl :: Ɐxs ∷ [Integer] → Bool
  foldrFoldl :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b -> SBV b) -> (SBV b -> SBV a -> SBV b) -> SBV b -> TP (Proof (Forall "xs" [a] -> SBool))
  foldrFoldl (<+>) (<*>) e = do
     -- Assumptions about the operators
     let -- (x <+> y) <*> z == x <+> (y <*> z)
         assoc = quantifiedBool $ \(Forall x) (Forall y) (Forall z) -> (x <+> y) <*> z .== x <+> (y <*> z)
  
         -- x <+> e == e <*> x
         unit  = quantifiedBool $ \(Forall x) -> x <+> e .== e <*> x
  
     -- Helper: x <+> foldl (<*>) y xs == foldl (<*>) (x <+> y) xs
     helper <-
        induct "foldl over <*>/<+>"
               (\(Forall @"xs" xs) (Forall @"x" x) (Forall @"y" y) -> assoc .=> x <+> foldl (<*>) y xs .== foldl (<*>) (x <+> y) xs) $
  
               -- Using z to avoid confusion with the variable x already present, following Bird.
               -- z3 can figure out the proper instantiation of ih so the at call is unnecessary, but being explicit is helpful.
               \ih (z, xs) x y -> [assoc] |- x <+> foldl (<*>) y (z .: xs)
                                          =: x <+> foldl (<*>) (y <*> z) xs
                                          ?? ih `at` (Inst @"x" x, Inst @"y" (y <*> z))
                                          =: foldl (<*>) (x <+> (y <*> z)) xs
                                          ?? assoc
                                          =: foldl (<*>) ((x <+> y) <*> z) xs
                                          =: foldl (<*>) (x <+> y) (z .: xs)
                                          =: qed
  
     -- Final proof:
     induct "foldrFoldl"
            (\(Forall xs) -> assoc .&& unit .=> foldr (<+>) e xs .== foldl (<*>) e xs) $
            \ih (x, xs) -> [assoc, unit] |- foldr (<+>) e (x .: xs)
                                         =: x <+> foldr (<+>) e xs
                                         ?? ih
                                         =: x <+> foldl (<*>) e xs
                                         ?? helper
                                         =: foldl (<*>) (x <+> e) xs
                                         =: foldl (<*>) (e <*> x) xs
                                         =: foldl (<*>) e (x .: xs)
                                         =: qed
  
  -- | Provided @f@ is associative and @a@ is its both left and right-unit:
  --
  -- @foldr f a . concat == foldr f a . map (foldr f a)@
  --
  -- >>> runTP $ bookKeeping @Integer (uninterpret "a") (uninterpret "f")
  -- Inductive lemma: foldBase
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Inductive lemma: foldrOverAppend
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Inductive lemma: bookKeeping
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Step: 6                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] bookKeeping :: Ɐxss ∷ [[Integer]] → Bool
  --
  -- NB. This theorem does not hold if @f@ does not have a left-unit! Consider the input @[[], [x]]@. Left hand side reduces to
  -- @x@, while the right hand side reduces to: @f a x@. And unless @f@ is commutative or @a@ is not also a left-unit,
  -- then one can find a counter-example. (Aside: if both left and right units exist for a binary operator, then they
  -- are necessarily the same element, since @l = f l r = r@. So, an equivalent statement could simply say @f@ has
  -- both left and right units.) A concrete counter-example is:
  --
  -- @
  --   data T = A | B | C
  --
  --   f :: T -> T -> T
  --   f C A = A
  --   f C B = A
  --   f x _ = x
  -- @
  --
  -- You can verify @f@ is associative. Also note that @C@ is the right-unit for @f@, but it isn't the left-unit.
  -- In fact, @f@ has no-left unit by the above argument. In this case, the bookkeeping law produces @B@ for
  -- the left-hand-side, and @A@ for the right-hand-side for the input @[[], [B]]@.
  bookKeeping :: forall a. SymVal a => SBV a -> (SBV a -> SBV a -> SBV a) -> TP (Proof (Forall "xss" [[a]] -> SBool))
  bookKeeping a f = do
  
     -- Assumptions about f
     let assoc = quantifiedBool $ \(Forall x) (Forall y) (Forall z) -> x `f` (y `f` z) .== (x `f` y) `f` z
         rUnit = quantifiedBool $ \(Forall x) -> x `f` a .== x
         lUnit = quantifiedBool $ \(Forall x) -> a `f` x .== x
  
     -- Helper: @foldr f y xs = foldr f a xs `f` y@
     helper <- induct "foldBase"
                      (\(Forall xs) (Forall y) -> lUnit .&& assoc .=> foldr f y xs .== foldr f a xs `f` y) $
                      \ih (x, xs) y -> [lUnit, assoc] |- foldr f y (x .: xs)
                                                      =: x `f` foldr f y xs
                                                      ?? ih
                                                      =: x `f` (foldr f a xs `f` y)
                                                      =: (x `f` foldr f a xs) `f` y
                                                      =: foldr f a (x .: xs) `f` y
                                                      =: qed
  
     foa <- foldrOverAppend a f
  
     induct "bookKeeping"
            (\(Forall xss) -> assoc .&& rUnit .&& lUnit .=> foldr f a (concat xss) .== foldr f a (map (foldr f a) xss)) $
            \ih (xs, xss) -> [assoc, rUnit, lUnit] |- foldr f a (concat (xs .: xss))
                                                   =: foldr f a (xs ++ concat xss)
                                                   ?? foa
                                                   =: foldr f (foldr f a (concat xss)) xs
                                                   ?? ih
                                                   =: foldr f (foldr f a (map (foldr f a) xss)) xs
                                                   ?? helper `at` (Inst @"xs" xs, Inst @"y" (foldr f a (map (foldr f a) xss)))
                                                   =: foldr f a xs `f` foldr f a (map (foldr f a) xss)
                                                   =: foldr f a (foldr f a xs .: map (foldr f a) xss)
                                                   =: foldr f a (map (foldr f a) (xs .: xss))
                                                   =: qed
  
  -- | @filter p (xs ++ ys) == filter p xs ++ filter p ys@
  --
  -- >>> runTP $ filterAppend @Integer (uninterpret "p")
  -- Inductive lemma: filterAppend
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] filterAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
  filterAppend :: forall a. SymVal a => (SBV a -> SBool) -> TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
  filterAppend p =
     induct "filterAppend"
            (\(Forall xs) (Forall ys) -> filter p xs ++ filter p ys .== filter p (xs ++ ys)) $
            \ih (x, xs) ys -> [] |- filter p (x .: xs) ++ filter p ys
                                 =: ite (p x) (x .: filter p xs) (filter p xs) ++ filter p ys
                                 =: ite (p x) (x .: filter p xs ++ filter p ys) (filter p xs ++ filter p ys)
                                 ?? ih
                                 =: ite (p x) (x .: filter p (xs ++ ys)) (filter p (xs ++ ys))
                                 =: filter p (x .: (xs ++ ys))
                                 =: filter p ((x .: xs) ++ ys)
                                 =: qed
  
  -- | @filter p (concat xss) == concatMap (filter p xss)@
  --
  -- >>> runTP $ filterConcat @Integer (uninterpret "f")
  -- Inductive lemma: filterAppend
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Inductive lemma: filterConcat
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] filterConcat :: Ɐxss ∷ [[Integer]] → Bool
  filterConcat :: forall a. SymVal a => (SBV a -> SBool) -> TP (Proof (Forall "xss" [[a]] -> SBool))
  filterConcat p = do
    fa <- filterAppend p
  
    inductWith cvc5 "filterConcat"
           (\(Forall xss) -> filter p (concat xss) .== concatMap (filter p) xss) $
           \ih (xs, xss) -> [] |- filter p (concat (xs .: xss))
                               =: filter p (xs ++ concat xss)
                               ?? fa
                               =: filter p xs ++ filter p (concat xss)
                               ?? ih
                               =: concatMap (filter p) (xs .: xss)
                               =: qed
  
  -- | @takeWhile f xs ++ dropWhile f xs == xs@
  --
  -- >>> runTP $ takeDropWhile @Integer (uninterpret "f")
  -- Inductive lemma: takeDropWhile
  --   Step: Base                            Q.E.D.
  --   Step: 1 (2 way case split)
  --     Step: 1.1.1                         Q.E.D.
  --     Step: 1.1.2                         Q.E.D.
  --     Step: 1.2.1                         Q.E.D.
  --     Step: 1.2.2                         Q.E.D.
  --     Step: 1.Completeness                Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] takeDropWhile :: Ɐxs ∷ [Integer] → Bool
  takeDropWhile :: forall a. SymVal a => (SBV a -> SBool) -> TP (Proof (Forall "xs" [a] -> SBool))
  takeDropWhile f =
     induct "takeDropWhile"
            (\(Forall xs) -> takeWhile f xs ++ dropWhile f xs .== xs) $
            \ih (x, xs) -> [] |- takeWhile f (x .: xs) ++ dropWhile f (x .: xs)
                              =: cases [ f x        ==> x .: takeWhile f xs ++ dropWhile f xs
                                                     ?? ih
                                                     =: x .: xs
                                                     =: qed
                                       , sNot (f x) ==> [] ++ x .: xs
                                                     =: x .: xs
                                                     =: qed
                                       ]
  -- | Remove adjacent duplicates.
  destutter :: SymVal a => SList a -> SList a
  destutter = smtFunction "destutter" $ \xs -> ite (null xs .|| null (tail xs))
                                                   xs
                                                   (let (a, as) = uncons xs
                                                        r       = destutter as
                                                    in ite (a .== head as) r (a .: r))
  
  -- | @destutter (destutter xs) == destutter xs@
  --
  -- >>> runTP $ destutterIdempotent @Integer
  -- Inductive lemma: helper1
  --   Step: Base                            Q.E.D.
  --   Step: 1 (2 way case split)
  --     Step: 1.1                           Q.E.D.
  --     Step: 1.2.1                         Q.E.D.
  --     Step: 1.2.2                         Q.E.D.
  --     Step: 1.Completeness                Q.E.D.
  --   Result:                               Q.E.D.
  -- Inductive lemma: helper2
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Inductive lemma (strong): helper3
  --   Step: Measure is non-negative         Q.E.D.
  --   Step: 1 (2 way full case split)
  --     Step: 1.1                           Q.E.D.
  --     Step: 1.2 (2 way full case split)
  --       Step: 1.2.1                       Q.E.D.
  --       Step: 1.2.2.1                     Q.E.D.
  --       Step: 1.2.2.2 (2 way case split)
  --         Step: 1.2.2.2.1.1               Q.E.D.
  --         Step: 1.2.2.2.1.2               Q.E.D.
  --         Step: 1.2.2.2.2.1               Q.E.D.
  --         Step: 1.2.2.2.2.2               Q.E.D.
  --         Step: 1.2.2.2.Completeness      Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: destutterIdempotent              Q.E.D.
  -- [Proven] destutterIdempotent :: Ɐxs ∷ [Integer] → Bool
  destutterIdempotent :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool))
  destutterIdempotent = do
  
     -- No adjacent duplicates
     let noAdd = smtFunction "noAdd" $ \xs -> null xs .|| null (tail xs) .|| (head xs ./= head (tail xs) .&& noAdd (tail xs))
  
     -- Helper: The head of a destuttered non-empty list does not change
     helper1 <- induct "helper1"
                       (\(Forall @"xs" (xs :: SList a)) (Forall @"h" h) -> head (destutter (h .: xs)) .== h) $
                       \ih (x, xs) h -> []
                                     |- head (destutter (h .: x .: xs))
                                     =: cases [ h ./= x ==> trivial
                                              , h .== x ==> head (destutter (x .: xs))
                                                         ?? ih
                                                         =: x
                                                         =: qed
                                              ]
  
     -- Helper: show that if a list has no adjacent duplicates, then destutter leaves it unchanged:
     helper2 <- induct "helper2"
                       (\(Forall @"xs" (xs :: SList a)) -> noAdd xs .=> destutter xs .== xs) $
                       \ih (x, xs) -> [noAdd (x .: xs)]
                                   |- destutter (x .: xs)
                                   ?? ih
                                   =: x .: xs
                                   =: qed
  
     -- Helper: prove that noAdd is true for the result of destutter
     helper3 <- sInductWith cvc5 "helper3"
                    (\(Forall @"xs" (xs :: SList a)) -> noAdd (destutter xs))
                    length $
                    \ih xs -> []
                           |- noAdd (destutter xs)
                           =: split xs
                                    trivial
                                    (\a as -> split as
                                                    trivial
                                                    (\b bs -> noAdd (destutter (a .: b .: bs))
                                                           =: cases [a .== b  ==> noAdd (destutter (b .: bs))
                                                                               ?? ih
                                                                               =: sTrue
                                                                               =: qed
                                                                    , a ./= b ==> noAdd (a .: destutter (b .: bs))
                                                                               ?? helper1 `at` (Inst @"xs" bs, Inst @"h" b)
                                                                               ?? ih
                                                                               =: sTrue
                                                                               =: qed
                                                                    ]))
  
     -- Now we can prove idempotency easily:
     lemma "destutterIdempotent"
            (\(Forall xs) -> destutter (destutter xs) .== destutter xs)
            [proofOf helper2, proofOf helper3]
  
  -- | @(as ++ bs) \\ cs == (as \\ cs) ++ (bs \\ cs)@
  --
  -- >>> runTP $ appendDiff @Integer
  -- Inductive lemma: appendDiff
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] appendDiff :: Ɐas ∷ [Integer] → Ɐbs ∷ [Integer] → Ɐcs ∷ [Integer] → Bool
  appendDiff :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "as" [a] -> Forall "bs" [a] -> Forall "cs" [a] -> SBool))
  appendDiff = induct "appendDiff"
                      (\(Forall as) (Forall bs) (Forall cs) -> (as ++ bs) \\ cs .== (as \\ cs) ++ (bs \\ cs)) $
                      \ih (a, as) bs cs -> [] |- (a .: as ++ bs) \\ cs
                                              =: (a .: (as ++ bs)) \\ cs
                                              =: ite (a `elem` cs) ((as ++ bs) \\ cs) (a .: ((as ++ bs) \\ cs))
                                              ?? ih
                                              =: ((a .: as) \\ cs) ++ (bs \\ cs)
                                              =: qed
  
  -- | @as \\ (bs ++ cs) == (as \\ bs) \\ cs@
  --
  -- >>> runTP $ diffAppend @Integer
  -- Inductive lemma: diffAppend
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] diffAppend :: Ɐas ∷ [Integer] → Ɐbs ∷ [Integer] → Ɐcs ∷ [Integer] → Bool
  diffAppend :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "as" [a] -> Forall "bs" [a] -> Forall "cs" [a] -> SBool))
  diffAppend = induct "diffAppend"
                      (\(Forall as) (Forall bs) (Forall cs) -> as \\ (bs ++ cs) .== (as \\ bs) \\ cs) $
                      \ih (a, as) bs cs -> [] |- (a .: as) \\ (bs ++ cs)
                                              =: ite (a `elem` (bs ++ cs)) (as \\ (bs ++ cs)) (a .: (as \\ (bs ++ cs)))
                                              ?? ih `at` (Inst @"bs" bs, Inst @"cs" cs)
                                              =: ite (a `elem` (bs ++ cs)) ((as \\ bs) \\ cs) (a .: (as \\ (bs ++ cs)))
                                              ?? ih `at` (Inst @"bs" bs, Inst @"cs" cs)
                                              =: ite (a `elem` (bs ++ cs)) ((as \\ bs) \\ cs) (a .: ((as \\ bs) \\ cs))
                                              =: ((a .: as) \\ bs) \\ cs
                                              =: qed
  
  -- | @(as \\ bs) \\ cs == (as \\ cs) \\ bs@
  --
  -- >>> runTP $ diffDiff @Integer
  -- Inductive lemma: diffDiff
  --   Step: Base                            Q.E.D.
  --   Step: 1 (2 way case split)
  --     Step: 1.1.1                         Q.E.D.
  --     Step: 1.1.2                         Q.E.D.
  --     Step: 1.1.3 (2 way case split)
  --       Step: 1.1.3.1                     Q.E.D.
  --       Step: 1.1.3.2.1                   Q.E.D.
  --       Step: 1.1.3.2.2 (a ∉ cs)          Q.E.D.
  --       Step: 1.1.3.Completeness          Q.E.D.
  --     Step: 1.2.1                         Q.E.D.
  --     Step: 1.2.2 (2 way case split)
  --       Step: 1.2.2.1.1                   Q.E.D.
  --       Step: 1.2.2.1.2                   Q.E.D.
  --       Step: 1.2.2.1.3 (a ∈ cs)          Q.E.D.
  --       Step: 1.2.2.2.1                   Q.E.D.
  --       Step: 1.2.2.2.2                   Q.E.D.
  --       Step: 1.2.2.2.3 (a ∉ bs)          Q.E.D.
  --       Step: 1.2.2.2.4 (a ∉ cs)          Q.E.D.
  --       Step: 1.2.2.Completeness          Q.E.D.
  --     Step: 1.Completeness                Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] diffDiff :: Ɐas ∷ [Integer] → Ɐbs ∷ [Integer] → Ɐcs ∷ [Integer] → Bool
  diffDiff :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "as" [a] -> Forall "bs" [a] -> Forall "cs" [a] -> SBool))
  diffDiff = induct "diffDiff"
                    (\(Forall as) (Forall bs) (Forall cs) -> (as \\ bs) \\ cs .== (as \\ cs) \\ bs) $
                    \ih (a, as) bs cs ->
                        [] |- ((a .: as) \\ bs) \\ cs
                           =: cases [ a `elem`    bs ==> (as \\ bs) \\ cs
                                                      ?? ih
                                                      =: (as \\ cs) \\ bs
                                                      =: cases [ a `elem`    cs ==> ((a .: as) \\ cs) \\ bs
                                                                                 =: qed
                                                               , a `notElem` cs ==> (a .: (as \\ cs)) \\ bs
                                                                                 ?? "a ∉ cs"
                                                                                 =: ((a .: as) \\ cs) \\ bs
                                                                                 =: qed
                                                               ]
                                    , a `notElem` bs ==> (a .: (as \\ bs)) \\ cs
                                                      =: cases [ a `elem`    cs ==> (as \\ bs) \\ cs
                                                                                 ?? ih
                                                                                 =: (as \\ cs) \\ bs
                                                                                 ?? "a ∈ cs"
                                                                                 =: ((a .: as) \\ cs) \\ bs
                                                                                 =: qed
                                                               , a `notElem` cs ==> a .: ((as \\ bs) \\ cs)
                                                                                 ?? ih
                                                                                 =: a .: ((as \\ cs) \\ bs)
                                                                                 ?? "a ∉ bs"
                                                                                 =: (a .: (as \\ cs)) \\ bs
                                                                                 ?? "a ∉ cs"
                                                                                 =: ((a .: as) \\ cs) \\ bs
                                                                                 =: qed
                                                               ]
                                    ]
  
  -- | Are the two lists disjoint?
  disjoint :: (Eq a, SymVal a) => SList a -> SList a -> SBool
  disjoint = smtFunction "disjoint" $ \xs ys -> null xs .|| head xs `notElem` ys .&& disjoint (tail xs) ys
  
  -- | @disjoint as bs .=> as \\ bs == as@
  --
  -- >>> runTP $ disjointDiff @Integer
  -- Inductive lemma: disjointDiff
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] disjointDiff :: Ɐas ∷ [Integer] → Ɐbs ∷ [Integer] → Bool
  disjointDiff :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "as" [a] -> Forall "bs" [a] -> SBool))
  disjointDiff = induct "disjointDiff"
                        (\(Forall as) (Forall bs) -> disjoint as bs .=> as \\ bs .== as) $
                        \ih (a, as) bs -> [disjoint (a .: as) bs]
                                       |- (a .: as) \\ bs
                                       =: a .: (as \\ bs)
                                       ?? ih
                                       =: a .: as
                                       =: qed
  
  -- | @fst (partition f xs) == filter f xs@
  --
  -- >>> runTP $ partition1 @Integer (uninterpret "f")
  -- Inductive lemma: partition1
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] partition1 :: Ɐxs ∷ [Integer] → Bool
  partition1 :: forall a. SymVal a => (SBV a -> SBool) -> TP (Proof (Forall "xs" [a] -> SBool))
  partition1 f =
     induct "partition1"
            (\(Forall xs) -> fst (partition f xs) .== filter f xs) $
            \ih (x, xs) -> [] |- fst (partition f (x .: xs))
                              =: fst (let res = partition f xs
                                      in ite (f x)
                                             (tuple (x .: fst res, snd res))
                                             (tuple (fst res, x .: snd res)))
                              =: ite (f x) (x .: fst (partition f xs)) (fst (partition f xs))
                              ?? ih
                              =: ite (f x) (x .: filter f xs) (filter f xs)
                              =: filter f (x .: xs)
                              =: qed
  
  -- | @snd (partition f xs) == filter (not . f) xs@
  --
  -- >>> runTP $ partition2 @Integer (uninterpret "f")
  -- Inductive lemma: partition2
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] partition2 :: Ɐxs ∷ [Integer] → Bool
  partition2 :: forall a. SymVal a => (SBV a -> SBool) -> TP (Proof (Forall "xs" [a] -> SBool))
  partition2 f =
     induct "partition2"
            (\(Forall xs) -> snd (partition f xs) .== filter (sNot . f) xs) $
            \ih (x, xs) -> [] |- snd (partition f (x .: xs))
                              =: snd (let res = partition f xs
                                      in ite (f x)
                                             (tuple (x .: fst res, snd res))
                                             (tuple (fst res, x .: snd res)))
                              =: ite (f x) (snd (partition f xs)) (x .: snd (partition f xs))
                              ?? ih
                              =: ite (f x) (filter (sNot . f) xs) (x .: filter (sNot . f) xs)
                              =: filter (sNot . f) (x .: xs)
                              =: qed
  
  -- | @take n (take m xs) == take (n `smin` m) xs@
  --
  -- >>> runTP $ take_take @Integer
  -- Lemma: take_take                        Q.E.D.
  -- [Proven] take_take :: Ɐm ∷ Integer → Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool
  take_take :: forall a. SymVal a => TP (Proof (Forall "m" Integer -> Forall "n" Integer -> Forall "xs" [a] -> SBool))
  take_take = lemma "take_take"
                    (\(Forall m) (Forall n) (Forall xs) -> take n (take m xs) .== take (n `smin` m) xs)
                    []
  
  -- | @n >= 0 && m >= 0 ==> drop n (drop m xs) == drop (n + m) xs@
  --
  -- >>> runTP $ drop_drop @Integer
  -- Lemma: drop_drop                        Q.E.D.
  -- [Proven] drop_drop :: Ɐm ∷ Integer → Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool
  drop_drop :: forall a. SymVal a => TP (Proof (Forall "m" Integer -> Forall "n" Integer -> Forall "xs" [a] -> SBool))
  drop_drop = lemma "drop_drop"
                    (\(Forall m) (Forall n) (Forall xs) -> n .>= 0 .&& m .>= 0 .=> drop n (drop m xs) .== drop (n + m) xs)
                    []
  
  -- | @take n xs ++ drop n xs == xs@
  --
  -- >>> runTP $ take_drop @Integer
  -- Lemma: take_drop                        Q.E.D.
  -- [Proven] take_drop :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool
  take_drop :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))
  take_drop = lemma "take_drop"
                    (\(Forall n) (Forall xs) -> take n xs ++ drop n xs .== xs)
                    []
  
  -- | @n .> 0 ==> take n (x .: xs) == x .: take (n - 1) xs@
  --
  -- >>> runTP $ take_cons @Integer
  -- Lemma: take_cons                        Q.E.D.
  -- [Proven] take_cons :: Ɐn ∷ Integer → Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool
  take_cons :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "x" a -> Forall "xs" [a] -> SBool))
  take_cons = lemma "take_cons"
                    (\(Forall n) (Forall x) (Forall xs) -> n .> 0 .=> take n (x .: xs) .== x .: take (n - 1) xs)
                    []
  
  -- | @take n (map f xs) == map f (take n xs)@
  --
  -- >>> runTP $ take_map @Integer @Integer (uninterpret "f")
  -- Lemma: take_cons                        Q.E.D.
  -- Lemma: map1                             Q.E.D.
  -- Lemma: take_map.n <= 0                  Q.E.D.
  -- Inductive lemma: take_map.n > 0
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: take_map
  --   Step: 1                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] take_map :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool
  take_map :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b) -> TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))
  take_map f = do
      tc   <- take_cons @a
  
      map1 <- lemma "map1"
                    (\(Forall x) (Forall xs) -> map f (x .: xs) .== f x .: map f xs)
                    []
  
      h1 <- lemma "take_map.n <= 0"
                   (\(Forall @"xs" xs) (Forall @"n" n) -> n .<= 0 .=> take n (map f xs) .== map f (take n xs))
                   []
  
      h2 <- induct "take_map.n > 0"
                   (\(Forall @"xs" xs) (Forall @"n" n) -> n .> 0 .=> take n (map f xs) .== map f (take n xs)) $
                   \ih (x, xs) n -> [n .> 0] |- take n (map f (x .: xs))
                                             =: take n (f x .: map f xs)
                                             =: f x .: take (n - 1) (map f xs)
                                             ?? ih `at` Inst @"n" (n-1)
                                             =: f x .: map f (take (n - 1) xs)
                                             ?? map1 `at` (Inst @"x" x, Inst @"xs" (take (n - 1) xs))
                                             =: map f (x .: take (n - 1) xs)
                                             ?? tc
                                             =: map f (take n (x .: xs))
                                             =: qed
  
      calc "take_map"
           (\(Forall n) (Forall xs) -> take n (map f xs) .== map f (take n xs)) $
           \n xs -> [] |- take n (map f xs)
                       ?? h1
                       ?? h2
                       =: map f (take n xs)
                       =: qed
  
  -- | @n .> 0 ==> drop n (x .: xs) == drop (n - 1) xs@
  --
  -- >>> runTP $ drop_cons @Integer
  -- Lemma: drop_cons                        Q.E.D.
  -- [Proven] drop_cons :: Ɐn ∷ Integer → Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool
  drop_cons :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "x" a -> Forall "xs" [a] -> SBool))
  drop_cons = lemma "drop_cons"
                    (\(Forall n) (Forall x) (Forall xs) -> n .> 0 .=> drop n (x .: xs) .== drop (n - 1) xs)
                    []
  
  -- | @drop n (map f xs) == map f (drop n xs)@
  --
  -- >>> runTP $ drop_map @Integer @String (uninterpret "f")
  -- Lemma: drop_cons                        Q.E.D.
  -- Lemma: drop_cons                        Q.E.D.
  -- Lemma: drop_map.n <= 0                  Q.E.D.
  -- Inductive lemma: drop_map.n > 0
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: drop_map
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] drop_map :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool
  drop_map :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b) -> TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))
  drop_map f = do
     dcA <- drop_cons @a
     dcB <- drop_cons @b
  
     h1 <- lemma "drop_map.n <= 0"
                 (\(Forall @"xs" xs) (Forall @"n" n) -> n .<= 0 .=> drop n (map f xs) .== map f (drop n xs))
                 []
  
     h2 <- induct "drop_map.n > 0"
                  (\(Forall @"xs" xs) (Forall @"n" n) -> n .> 0 .=> drop n (map f xs) .== map f (drop n xs)) $
                  \ih (x, xs) n -> [n .> 0] |- drop n (map f (x .: xs))
                                            =: drop n (f x .: map f xs)
                                            ?? dcB `at` (Inst @"n" n, Inst @"x" (f x), Inst @"xs" (map f xs))
                                            =: drop (n - 1) (map f xs)
                                            ?? ih `at` Inst @"n" (n-1)
                                            =: map f (drop (n - 1) xs)
                                            ?? dcA `at` (Inst @"n" n, Inst @"x" x, Inst @"xs" xs)
                                            =: map f (drop n (x .: xs))
                                            =: qed
  
     -- I'm a bit surprised that z3 can't deduce the following with a simple-lemma, which is essentially a simple case-split.
     -- But the good thing about calc is that it lets us direct the tool in precise ways that we'd like.
     calc "drop_map"
          (\(Forall n) (Forall xs) -> drop n (map f xs) .== map f (drop n xs)) $
          \n xs -> [] |- let result = drop n (map f xs) .== map f (drop n xs)
                         in result
                         =: ite (n .<= 0) (n .<= 0 .=> result) (n .> 0 .=> result)
                         ?? h1
                         =: ite (n .<= 0) sTrue (n .> 0 .=> result)
                         ?? h2
                         =: ite (n .<= 0) sTrue sTrue
                         =: sTrue
                         =: qed
  
  -- | @n >= 0 ==> length (take n xs) == length xs \`min\` n@
  --
  -- >>> runTP $ length_take @Integer
  -- Lemma: length_take                      Q.E.D.
  -- [Proven] length_take :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool
  length_take :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))
  length_take = lemma "length_take"
                      (\(Forall n) (Forall xs) -> n .>= 0 .=> length (take n xs) .== length xs `smin` n)
                      []
  
  -- | @n >= 0 ==> length (drop n xs) == (length xs - n) \`max\` 0@
  --
  -- >>> runTP $ length_drop @Integer
  -- Lemma: length_drop                      Q.E.D.
  -- [Proven] length_drop :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool
  length_drop :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))
  length_drop = lemma "length_drop"
                      (\(Forall n) (Forall xs) -> n .>= 0 .=> length (drop n xs) .== (length xs - n) `smax` 0)
                      []
  
  -- | @length xs \<= n ==\> take n xs == xs@
  --
  -- >>> runTP $ take_all @Integer
  -- Lemma: take_all                         Q.E.D.
  -- [Proven] take_all :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool
  take_all :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))
  take_all = lemma "take_all"
                   (\(Forall n) (Forall xs) -> length xs .<= n .=> take n xs .== xs)
                   []
  
  -- | @length xs \<= n ==\> drop n xs == nil@
  --
  -- >>> runTP $ drop_all @Integer
  -- Lemma: drop_all                         Q.E.D.
  -- [Proven] drop_all :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Bool
  drop_all :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool))
  drop_all = lemma "drop_all"
                   (\(Forall n) (Forall xs) -> length xs .<= n .=> drop n xs .== nil)
                   []
  
  -- | @take n (xs ++ ys) == (take n xs ++ take (n - length xs) ys)@
  --
  -- >>> runTP $ take_append @Integer
  -- Lemma: take_append                      Q.E.D.
  -- [Proven] take_append :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
  take_append :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))
  take_append = lemmaWith cvc5 "take_append"
                          (\(Forall n) (Forall xs) (Forall ys) -> take n (xs ++ ys) .== take n xs ++ take (n - length xs) ys)
                          []
  
  -- | @drop n (xs ++ ys) == drop n xs ++ drop (n - length xs) ys@
  --
  -- NB. As of Feb 2025, z3 struggles to prove this, but cvc5 gets it out-of-the-box.
  --
  -- >>> runTP $ drop_append @Integer
  -- Lemma: drop_append                      Q.E.D.
  -- [Proven] drop_append :: Ɐn ∷ Integer → Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
  drop_append :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))
  drop_append = lemmaWith cvc5 "drop_append"
                          (\(Forall n) (Forall xs) (Forall ys) -> drop n (xs ++ ys) .== drop n xs ++ drop (n - length xs) ys)
                          []
  
  -- | @length xs == length ys ==> map fst (zip xs ys) = xs@
  --
  -- >>> runTP $ map_fst_zip @Integer @Integer
  -- Inductive lemma: map_fst_zip
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] map_fst_zip :: (Ɐxs ∷ [Integer], Ɐys ∷ [Integer]) → Bool
  map_fst_zip :: forall a b. (SymVal a, SymVal b) => TP (Proof ((Forall "xs" [a], Forall "ys" [b]) -> SBool))
  map_fst_zip = induct "map_fst_zip"
                       (\(Forall xs, Forall ys) -> length xs .== length ys .=> map fst (zip xs ys) .== xs) $
                       \ih (x, xs, y, ys) -> [length (x .: xs) .== length (y .: ys)]
                                          |- map fst (zip (x .: xs) (y .: ys))
                                          =: map fst (tuple (x, y) .: zip xs ys)
                                          =: fst (tuple (x, y)) .: map fst (zip xs ys)
                                          =: x .: map fst (zip xs ys)
                                          ?? ih
                                          =: x .: xs
                                          =: qed
  
  -- | @length xs == length ys ==> map snd (zip xs ys) = xs@
  --
  -- >>> runTP $ map_snd_zip @Integer @Integer
  -- Inductive lemma: map_snd_zip
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] map_snd_zip :: (Ɐxs ∷ [Integer], Ɐys ∷ [Integer]) → Bool
  map_snd_zip :: forall a b. (SymVal a, SymVal b) => TP (Proof ((Forall "xs" [a], Forall "ys" [b]) -> SBool))
  map_snd_zip = induct "map_snd_zip"
                       (\(Forall xs, Forall ys) -> length xs .== length ys .=> map snd (zip xs ys) .== ys) $
                       \ih (x, xs, y, ys) -> [length (x .: xs) .== length (y .: ys)]
                                          |- map snd (zip (x .: xs) (y .: ys))
                                          =: map snd (tuple (x, y) .: zip xs ys)
                                          =: snd (tuple (x, y)) .: map snd (zip xs ys)
                                          =: y .: map snd (zip xs ys)
                                          ?? ih
                                          =: y .: ys
                                          =: qed
  
  -- | @map fst (zip xs ys) == take (min (length xs) (length ys)) xs@
  --
  -- >>> runTP $ map_fst_zip_take @Integer @Integer
  -- Lemma: take_cons                        Q.E.D.
  -- Inductive lemma: map_fst_zip_take
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] map_fst_zip_take :: (Ɐxs ∷ [Integer], Ɐys ∷ [Integer]) → Bool
  map_fst_zip_take :: forall a b. (SymVal a, SymVal b) => TP (Proof ((Forall "xs" [a], Forall "ys" [b]) -> SBool))
  map_fst_zip_take = do
     tc <- take_cons @a
  
     induct "map_fst_zip_take"
            (\(Forall xs, Forall ys) -> map fst (zip xs ys) .== take (length xs `smin` length ys) xs) $
            \ih (x, xs, y, ys) -> [] |- map fst (zip (x .: xs) (y .: ys))
                                     =: map fst (tuple (x, y) .: zip xs ys)
                                     =: x .: map fst (zip xs ys)
                                     ?? ih
                                     =: x .: take (length xs `smin` length ys) xs
                                     ?? tc
                                     =: take (1 + (length xs `smin` length ys)) (x .: xs)
                                     =: take (length (x .: xs) `smin` length (y .: ys)) (x .: xs)
                                     =: qed
  
  -- | @map snd (zip xs ys) == take (min (length xs) (length ys)) xs@
  --
  -- >>> runTP $ map_snd_zip_take @Integer @Integer
  -- Lemma: take_cons                        Q.E.D.
  -- Inductive lemma: map_snd_zip_take
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] map_snd_zip_take :: (Ɐxs ∷ [Integer], Ɐys ∷ [Integer]) → Bool
  map_snd_zip_take :: forall a b. (SymVal a, SymVal b) => TP (Proof ((Forall "xs" [a], Forall "ys" [b]) -> SBool))
  map_snd_zip_take = do
     tc <- take_cons @a
  
     induct "map_snd_zip_take"
            (\(Forall xs, Forall ys) -> map snd (zip xs ys) .== take (length xs `smin` length ys) ys) $
            \ih (x, xs, y, ys) -> [] |- map snd (zip (x .: xs) (y .: ys))
                                     =: map snd (tuple (x, y) .: zip xs ys)
                                     =: y .: map snd (zip xs ys)
                                     ?? ih
                                     =: y .: take (length xs `smin` length ys) ys
                                     ?? tc
                                     =: take (1 + (length xs `smin` length ys)) (y .: ys)
                                     =: take (length (x .: xs) `smin` length (y .: ys)) (y .: ys)
                                     =: qed
  
  -- | Count the number of occurrences of an element in a list
  count :: SymVal a => SBV a -> SList a -> SInteger
  count = smtFunction "count" $ \e l -> ite (null l)
                                            0
                                            (let (x, xs) = uncons l
                                                 cxs     = count e xs
                                             in ite (e .== x) (1 + cxs) cxs)
  
  -- | Interleave the elements of two lists. If one ends, we take the rest from the other.
  interleave :: SymVal a => SList a -> SList a -> SList a
  interleave = smtFunction "interleave" (\xs ys -> ite (null  xs) ys (head xs .: interleave ys (tail xs)))
  
  -- | Prove that interleave preserves total length.
  --
  -- The induction here is on the total length of the lists, and hence
  -- we use the generalized induction principle. We have:
  --
  -- >>> runTP $ interleaveLen @Integer
  -- Inductive lemma (strong): interleaveLen
  --   Step: Measure is non-negative         Q.E.D.
  --   Step: 1 (2 way full case split)
  --     Step: 1.1                           Q.E.D.
  --     Step: 1.2.1                         Q.E.D.
  --     Step: 1.2.2                         Q.E.D.
  --     Step: 1.2.3                         Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] interleaveLen :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
  interleaveLen :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
  interleaveLen = sInduct "interleaveLen"
                          (\(Forall xs) (Forall ys) -> length xs + length ys .== length (interleave xs ys))
                          (\xs ys -> length xs + length ys) $
                          \ih xs ys -> [] |- length xs + length ys .== length (interleave xs ys)
                                          =: split xs
                                                   trivial
                                                   (\a as -> length (a .: as) + length ys .== length (interleave (a .: as) ys)
                                                          =: 1 + length as + length ys .== 1 + length (interleave ys as)
                                                          ?? ih `at` (Inst @"xs" ys, Inst @"ys" as)
                                                          =: sTrue
                                                          =: qed)
  
  -- | Uninterleave the elements of two lists. We roughly split it into two, of alternating elements.
  uninterleave :: SymVal a => SList a -> STuple [a] [a]
  uninterleave lst = uninterleaveGen lst (tuple (nil, nil))
  
  -- | Generalized form of uninterleave with the auxilary lists made explicit.
  uninterleaveGen :: SymVal a => SList a -> STuple [a] [a] -> STuple [a] [a]
  uninterleaveGen = smtFunction "uninterleave" (\xs alts -> let (es, os) = untuple alts
                                                            in ite (null xs)
                                                                   (tuple (reverse es, reverse os))
                                                                   (uninterleaveGen (tail xs) (tuple (os, head xs .: es))))
  
  -- | The functions 'uninterleave' and 'interleave' are inverses so long as the inputs are of the same length. (The equality
  -- would even hold if the first argument has one extra element, but we keep things simple here.)
  --
  -- We have:
  --
  -- >>> runTP $ interleaveRoundTrip @Integer
  -- Lemma: revCons                          Q.E.D.
  -- Inductive lemma (strong): roundTripGen
  --   Step: Measure is non-negative         Q.E.D.
  --   Step: 1 (4 way full case split)
  --     Step: 1.1                           Q.E.D.
  --     Step: 1.2                           Q.E.D.
  --     Step: 1.3                           Q.E.D.
  --     Step: 1.4.1                         Q.E.D.
  --     Step: 1.4.2                         Q.E.D.
  --     Step: 1.4.3                         Q.E.D.
  --     Step: 1.4.4                         Q.E.D.
  --     Step: 1.4.5                         Q.E.D.
  --     Step: 1.4.6                         Q.E.D.
  --     Step: 1.4.7                         Q.E.D.
  --     Step: 1.4.8                         Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: interleaveRoundTrip
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] interleaveRoundTrip :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool
  interleaveRoundTrip :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))
  interleaveRoundTrip = do
  
     revHelper <- lemma "revCons" (\(Forall a) (Forall as) (Forall bs) -> reverse @a (a .: as) ++ bs .== reverse as ++ (a .: bs)) []
  
     -- Generalize the theorem first to take the helper lists explicitly
     roundTripGen <- sInductWith cvc5
           "roundTripGen"
           (\(Forall @"xs" xs) (Forall @"ys" ys) (Forall @"alts" alts) ->
                 length xs .== length ys .=> let (es, os) = untuple alts
                                             in uninterleaveGen (interleave xs ys) alts .== tuple (reverse es ++ xs, reverse os ++ ys))
           (\xs ys _alts -> length xs + length ys) $
           \ih xs ys alts -> [length xs .== length ys]
                          |- let (es, os) = untuple alts
                          in uninterleaveGen (interleave xs ys) alts
                          =: split2 (xs, ys)
                                    trivial
                                    trivial
                                    trivial
                                    (\(a, as) (b, bs) -> uninterleaveGen (interleave (a .: as) (b .: bs)) alts
                                                      =: uninterleaveGen (a .: interleave (b .: bs) as) alts
                                                      =: uninterleaveGen (a .: b .: interleave as bs) alts
                                                      =: uninterleaveGen (interleave as bs) (tuple (a .: es, b .: os))
                                                      ?? ih `at` (Inst @"xs" as, Inst @"ys" bs, Inst @"alts" (tuple (a .: es, b .: os)))
                                                      =: tuple (reverse (a .: es) ++ as, reverse (b .: os) ++ bs)
                                                      ?? revHelper `at` (Inst @"a" a, Inst @"as" es, Inst @"bs" as)
                                                      =: tuple (reverse es ++ (a .: as), reverse (b .: os) ++ bs)
                                                      ?? revHelper `at` (Inst @"a" b, Inst @"as" os, Inst @"bs" bs)
                                                      =: tuple (reverse es ++ (a .: as), reverse os ++ (b .: bs))
                                                      =: tuple (reverse es ++ xs, reverse os ++ ys)
                                                      =: qed)
  
     -- Round-trip theorem:
     calc "interleaveRoundTrip"
             (\(Forall xs) (Forall ys) -> length xs .== length ys .=> uninterleave (interleave xs ys) .== tuple (xs, ys)) $
             \xs ys -> [length xs .== length ys]
                    |- uninterleave (interleave xs ys)
                    =: uninterleaveGen (interleave xs ys) (tuple (nil, nil))
                    ?? roundTripGen `at` (Inst @"xs" xs, Inst @"ys" ys, Inst @"alts" (tuple (nil, nil)))
                    =: tuple (reverse nil ++ xs, reverse nil ++ ys)
                    =: qed
  
  -- | @count e (xs ++ ys) == count e xs + count e ys@
  --
  -- >>> runTP $ countAppend @Integer
  -- Inductive lemma: countAppend
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2 (unfold count)                Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4 (simplify)                    Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] countAppend :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Ɐe ∷ Integer → Bool
  countAppend :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> Forall "e" a -> SBool))
  countAppend =
     induct "countAppend"
            (\(Forall xs) (Forall ys) (Forall e) -> count e (xs ++ ys) .== count e xs + count e ys) $
            \ih (x, xs) ys e -> [] |- count e ((x .: xs) ++ ys)
                                   =: count e (x .: (xs ++ ys))
                                   ?? "unfold count"
                                   =: (let r = count e (xs ++ ys) in ite (e .== x) (1+r) r)
                                   ?? ih `at` (Inst @"ys" ys, Inst @"e" e)
                                   =: (let r = count e xs + count e ys in ite (e .== x) (1+r) r)
                                   ?? "simplify"
                                   =: count e (x .: xs) + count e ys
                                   =: qed
  
  -- | @count e (take n xs) + count e (drop n xs) == count e xs@
  --
  -- >>> runTP $ takeDropCount @Integer
  -- Inductive lemma: countAppend
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2 (unfold count)                Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4 (simplify)                    Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: take_drop                        Q.E.D.
  -- Lemma: takeDropCount
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] takeDropCount :: Ɐxs ∷ [Integer] → Ɐn ∷ Integer → Ɐe ∷ Integer → Bool
  takeDropCount :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "n" Integer -> Forall "e" a -> SBool))
  takeDropCount = do
         capp     <- countAppend @a
         takeDrop <- take_drop   @a
  
         calc "takeDropCount"
              (\(Forall xs) (Forall n) (Forall e) -> count e (take n xs) + count e (drop n xs) .== count e xs) $
              \xs n e -> [] |- count e (take n xs) + count e (drop n xs)
                            ?? capp `at` (Inst @"xs" (take n xs), Inst @"ys" (drop n xs), Inst @"e" e)
                            =: count e (take n xs ++ drop n xs)
                            ?? takeDrop
                            =: count e xs
                            =: qed
  
  -- | @count e xs >= 0@
  --
  -- >>> runTP $ countNonNeg @Integer
  -- Inductive lemma: countNonNeg
  --   Step: Base                            Q.E.D.
  --   Step: 1 (2 way case split)
  --     Step: 1.1.1                         Q.E.D.
  --     Step: 1.1.2                         Q.E.D.
  --     Step: 1.2.1                         Q.E.D.
  --     Step: 1.2.2                         Q.E.D.
  --     Step: 1.Completeness                Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] countNonNeg :: Ɐxs ∷ [Integer] → Ɐe ∷ Integer → Bool
  countNonNeg :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> Forall "e" a -> SBool))
  countNonNeg =
     induct "countNonNeg"
            (\(Forall xs) (Forall e) -> count e xs .>= 0) $
            \ih (x, xs) e -> [] |- count e (x .: xs) .>= 0
                                =: cases [ e .== x ==> 1 + count e xs .>= 0
                                                    ?? ih
                                                    =: sTrue
                                                    =: qed
                                         , e ./= x ==> count e xs .>= 0
                                                    ?? ih
                                                    =: sTrue
                                                    =: qed
                                         ]
  
  -- | @e \`elem\` xs ==> count e xs .> 0@
  --
  -- >>> runTP $ countElem @Integer
  -- Inductive lemma: countNonNeg
  --   Step: Base                            Q.E.D.
  --   Step: 1 (2 way case split)
  --     Step: 1.1.1                         Q.E.D.
  --     Step: 1.1.2                         Q.E.D.
  --     Step: 1.2.1                         Q.E.D.
  --     Step: 1.2.2                         Q.E.D.
  --     Step: 1.Completeness                Q.E.D.
  --   Result:                               Q.E.D.
  -- Inductive lemma: countElem
  --   Step: Base                            Q.E.D.
  --   Step: 1 (2 way case split)
  --     Step: 1.1.1                         Q.E.D.
  --     Step: 1.1.2                         Q.E.D.
  --     Step: 1.2.1                         Q.E.D.
  --     Step: 1.2.2                         Q.E.D.
  --     Step: 1.Completeness                Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] countElem :: Ɐxs ∷ [Integer] → Ɐe ∷ Integer → Bool
  countElem :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "xs" [a] -> Forall "e" a -> SBool))
  countElem = do
  
      cnn <- countNonNeg @a
  
      induct "countElem"
             (\(Forall xs) (Forall e) -> e `elem` xs .=> count e xs .> 0) $
             \ih (x, xs) e -> [e `elem` (x .: xs)]
                           |- count e (x .: xs) .> 0
                           =: cases [ e .== x ==> 1 + count e xs .> 0
                                               ?? cnn
                                               =: sTrue
                                               =: qed
                                    , e ./= x ==> count e xs .> 0
                                               ?? ih
                                               =: sTrue
                                               =: qed
                                    ]
  
  -- | @count e xs .> 0 .=> e \`elem\` xs@
  --
  -- >>> runTP $ elemCount @Integer
  -- Inductive lemma: elemCount
  --   Step: Base                            Q.E.D.
  --   Step: 1 (2 way case split)
  --     Step: 1.1                           Q.E.D.
  --     Step: 1.2.1                         Q.E.D.
  --     Step: 1.2.2                         Q.E.D.
  --     Step: 1.Completeness                Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] elemCount :: Ɐxs ∷ [Integer] → Ɐe ∷ Integer → Bool
  elemCount :: forall a. (Eq a, SymVal a) => TP (Proof (Forall "xs" [a] -> Forall "e" a -> SBool))
  elemCount =
      induct "elemCount"
             (\(Forall xs) (Forall e) -> count e xs .> 0 .=> e `elem` xs) $
             \ih (x, xs) e -> [count e xs .> 0]
                           |- e `elem` (x .: xs)
                           =: cases [ e .== x ==> trivial
                                    , e ./= x ==> e `elem` xs
                                               ?? ih
                                               =: sTrue
                                               =: qed
                                    ]
  
  {- HLint ignore revRev         "Redundant reverse" -}
  {- HLint ignore allAny         "Use and"           -}
  {- HLint ignore bookKeeping    "Fuse foldr/map"    -}
  {- HLint ignore foldrMapFusion "Fuse foldr/map"    -}
  {- HLint ignore filterConcat   "Move filter"       -}
  {- HLint ignore module         "Use camelCase"     -}
  {- HLint ignore module         "Use first"         -}
  {- HLint ignore module         "Use second"        -}
  {- HLint ignore module         "Use zipWith"       -}
  {- HLint ignore mapCompose     "Use map once"      -}
  {- HLint ignore tailsAppend    "Avoid lambda"      -}
  {- HLint ignore tailsAppend    "Use :"             -}
  {- HLint ignore mapReverse     "Evaluate"          -}
  {- HLint ignore takeDropWhile  "Evaluate"          -}
  