From 343a23d2bb675b38196ab6064b1aec895d3bf4c3 Mon Sep 17 00:00:00 2001
From: Levent Erkok <erkokl@gmail.com>
Date: Mon, 9 Dec 2024 17:43:15 -0800
Subject: [PATCH] generalize the proof

---
 Documentation/SBV/Examples/KnuckleDragger/Lists.hs | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/Documentation/SBV/Examples/KnuckleDragger/Lists.hs b/Documentation/SBV/Examples/KnuckleDragger/Lists.hs
index dd029625..4022207a 100644
--- a/Documentation/SBV/Examples/KnuckleDragger/Lists.hs
+++ b/Documentation/SBV/Examples/KnuckleDragger/Lists.hs
@@ -97,10 +97,15 @@ revCons = runKD $ do
 -- [Proven] mapAppend
 mapAppend :: (SA -> SB) -> IO Proof
 mapAppend f = runKD $ do
-   let p :: SList A -> SBool
-       p xs = quantifiedBool $ \(Forall @"ys" ys) -> map f (xs ++ ys) .== map f xs ++ map f ys
+   let p :: SList A -> SList A -> SBool
+       p xs ys = map f (xs ++ ys) .== map f xs ++ map f ys
 
-   lemma "mapAppend" (\(Forall @"xs" xs) -> p xs) [induct p]
+       genP :: SList A -> SBool
+       genP xs = quantifiedBool $ \(Forall @"ys" ys) -> p xs ys
+
+   gma <- lemma "genMapAppend" (\(Forall @"xs" xs) -> genP xs) [induct genP]
+
+   lemma "genAppend" (\(Forall @"xs" xs) (Forall @"ys" ys) -> p xs ys) [gma]
 
 -- | @map f . reverse == reverse . map f@
 --
@@ -121,9 +126,6 @@ mapReverse = runKD $ do
      let f :: SA -> SB
          f = uninterpret "f"
 
-the problem here is that the mapAppend now has a nested quantifier, which messes things up..
-hmm.
-
          p :: SList A -> SBool
          p xs = reverse (map f xs) .== map f (reverse xs)