diff --git a/src/Control/NCurses.idr b/src/Control/NCurses.idr
index 1333cd2..28928f1 100644
--- a/src/Control/NCurses.idr
+++ b/src/Control/NCurses.idr
@@ -176,17 +176,23 @@ inWindow = InWindow
 -- ^ NOTE: This _should_ be possible to do provably without creating a new @InWindow@ constructor just by
 --         using @SetWindow@ twice but I have yet to get the proofs to work.
 
+public export
+hasWindowWithin' : InWindow w s -> HasWindow w s
+hasWindowWithin' {s = (Active _ _ ((MkWindow name _ _) ** Here) _)} IsCurrentWindow = ItHasWindow
+hasWindowWithin' {s = (Active i (y :: xs) ((MkWindow name k d) ** (There x)) c)} p@(IsCurrentWindow) =
+  let c' : InWindow name (Active i xs ((MkWindow name k d) ** x) c) = IsCurrentWindow
+  in moreWindowsHasWindow @{hasWindowWithin' (assert_smaller p c')}
+
 public export
 %hint
 hasWindowWithin : InWindow w s => HasWindow w s
-hasWindowWithin {s = (Active _ _ ((MkWindow name _ _) ** Here) _)} @{IsCurrentWindow} = ItHasWindow
-hasWindowWithin {s = (Active _ _ ((MkWindow name _ _) ** (There x)) _)} @{IsCurrentWindow} = hasWindowWithin
+hasWindowWithin @{p} = hasWindowWithin' p
 
 public export
 %hint
 identifiesCurrentWindow : InWindow w (Active _ ws _ _) => IdentifiesWindow w ws
-identifiesCurrentWindow {ws} @{p} with (hasWindowWithin @{p})
-  identifiesCurrentWindow {ws} @{p} | (ItHasWindow @{ident}) = ident
+identifiesCurrentWindow @{p} with (hasWindowWithin @{p})
+  identifiesCurrentWindow @{p} | (ItHasWindow @{ident}) = ident
 
 ||| If a given state has a window, setting a new current window on that state does not
 ||| change the fact that the state has the original window.
diff --git a/src/Control/NCurses/State.idr b/src/Control/NCurses/State.idr
index fa0f56b..9b0070a 100644
--- a/src/Control/NCurses/State.idr
+++ b/src/Control/NCurses/State.idr
@@ -319,6 +319,12 @@ namespace Window
   data HasWindow : (0 name : String) -> CursesState -> Type where
     ItHasWindow : IdentifiesWindow name ws => HasWindow name (Active _ ws _ _)
 
+  public export
+  moreWindowsHasWindow : HasWindow name (Active i xs (MkWindow name k d ** x) c) =>
+                         HasWindow name (Active i (y :: xs) (MkWindow name k d ** There x) c)
+  moreWindowsHasWindow {xs = (MkWindow name _ _ :: windows)} @{ItHasWindow @{Here}} = ItHasWindow
+  moreWindowsHasWindow {xs = (w :: windows)} @{ItHasWindow @{(There z)}} = ItHasWindow
+
   public export %inline
   DefaultWindow : String
   DefaultWindow = "default"