-- SPDX-FileCopyrightText: 2022 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

{-# OPTIONS_HADDOCK not-home #-}

-- | Module, containing some internally used typelevel proofs.
module Morley.Michelson.Typed.Instr.Internal.Proofs
  ( module Morley.Michelson.Typed.Instr.Internal.Proofs
  ) where

import Prelude hiding (EQ, GT, LT)

import Data.Constraint (Dict(..), (\\))
import Data.Type.Equality ((:~:)(..))

import Morley.Michelson.Typed.Instr.Constraints
import Morley.Michelson.Typed.TypeLevel
import Morley.Util.Peano
import Morley.Util.PeanoNatural
import Morley.Util.StubbedProof
import Morley.Util.Type (KList(..), type (++))

assocThm :: forall a b c. (a ++ b) ++ c :~: a ++ (b ++ c)
assocThm :: forall {k} (a :: [k]) (b :: [k]) (c :: [k]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
assocThm = (Stubbed => ((a ++ b) ++ c) :~: (a ++ (b ++ c)))
-> ((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => ((a ++ b) ++ c) :~: (a ++ (b ++ c)))
 -> ((a ++ b) ++ c) :~: (a ++ (b ++ c)))
-> (Stubbed => ((a ++ b) ++ c) :~: (a ++ (b ++ c)))
-> ((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall a b. (a -> b) -> a -> b
$ case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
forall {k} (xs :: [k]). KList xs
assumeKnown @a of
  KList a
KNil -> (b ++ c) :~: (b ++ c)
((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall {k} (a :: k). a :~: a
Refl
  KCons Proxy x
_ (Proxy xs
_ :: Proxy xs) -> (x : (xs ++ (b ++ c))) :~: (x : (xs ++ (b ++ c)))
(x : ((xs ++ b) ++ c)) :~: (x : (xs ++ (b ++ c)))
(((xs ++ b) ++ c) ~ (xs ++ (b ++ c))) =>
(x : ((xs ++ b) ++ c)) :~: (x : (xs ++ (b ++ c)))
forall {k} (a :: k). a :~: a
Refl ((((xs ++ b) ++ c) ~ (xs ++ (b ++ c))) =>
 (x : ((xs ++ b) ++ c)) :~: (x : (xs ++ (b ++ c))))
-> (((xs ++ b) ++ c) :~: (xs ++ (b ++ c)))
-> (x : ((xs ++ b) ++ c)) :~: (x : (xs ++ (b ++ c)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [k]) (b :: [k]) (c :: [k]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall {k} (a :: [k]) (b :: [k]) (c :: [k]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
assocThm @xs @b @c

takeExtensionThm
  :: forall a s n. IsLongerOrSameLength a n ~ 'True
  => PeanoNatural n
  -> LazyTake n (a ++ s) :~: LazyTake n a
takeExtensionThm :: forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
takeExtensionThm PeanoNatural n
n = (Stubbed => LazyTake n (a ++ s) :~: LazyTake n a)
-> LazyTake n (a ++ s) :~: LazyTake n a
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => LazyTake n (a ++ s) :~: LazyTake n a)
 -> LazyTake n (a ++ s) :~: LazyTake n a)
-> (Stubbed => LazyTake n (a ++ s) :~: LazyTake n a)
-> LazyTake n (a ++ s) :~: LazyTake n a
forall a b. (a -> b) -> a -> b
$ case PeanoNatural n
n of
  PeanoNatural n
Zero -> '[] :~: '[]
LazyTake n (a ++ s) :~: LazyTake n a
forall {k} (a :: k). a :~: a
Refl
  Succ PeanoNatural m
m -> case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
forall {k} (xs :: [k]). KList xs
assumeKnown @a of
    KCons Proxy x
_ (Proxy xs
_ :: Proxy xs) -> (x : LazyTake m xs) :~: (x : LazyTake m xs)
(x : LazyTake m (xs ++ s)) :~: (x : LazyTake m xs)
(LazyTake m (xs ++ s) ~ LazyTake m xs) =>
(x : LazyTake m (xs ++ s)) :~: (x : LazyTake m xs)
forall {k} (a :: k). a :~: a
Refl ((LazyTake m (xs ++ s) ~ LazyTake m xs) =>
 (x : LazyTake m (xs ++ s)) :~: (x : LazyTake m xs))
-> (LazyTake m (xs ++ s) :~: LazyTake m xs)
-> (x : LazyTake m (xs ++ s)) :~: (x : LazyTake m xs)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
takeExtensionThm @xs @s PeanoNatural m
m

dropExtensionThm
  :: forall a s n. IsLongerOrSameLength a n ~ 'True
  => PeanoNatural n
  -> Drop n (a ++ s) :~: Drop n a ++ s
dropExtensionThm :: forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
dropExtensionThm PeanoNatural n
n = (Stubbed => Drop n (a ++ s) :~: (Drop n a ++ s))
-> Drop n (a ++ s) :~: (Drop n a ++ s)
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => Drop n (a ++ s) :~: (Drop n a ++ s))
 -> Drop n (a ++ s) :~: (Drop n a ++ s))
-> (Stubbed => Drop n (a ++ s) :~: (Drop n a ++ s))
-> Drop n (a ++ s) :~: (Drop n a ++ s)
forall a b. (a -> b) -> a -> b
$ case PeanoNatural n
n of
  PeanoNatural n
Zero -> (a ++ s) :~: (a ++ s)
Drop n (a ++ s) :~: (Drop n a ++ s)
forall {k} (a :: k). a :~: a
Refl
  Succ PeanoNatural m
m -> case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
forall {k} (xs :: [k]). KList xs
assumeKnown @a of
    KCons Proxy x
_ (Proxy xs
_ :: Proxy xs) -> (Drop m xs ++ s) :~: (Drop m xs ++ s)
Drop m (xs ++ s) :~: (Drop m xs ++ s)
(Drop m (xs ++ s) ~ (Drop m xs ++ s)) =>
Drop m (xs ++ s) :~: (Drop m xs ++ s)
forall {k} (a :: k). a :~: a
Refl ((Drop m (xs ++ s) ~ (Drop m xs ++ s)) =>
 Drop m (xs ++ s) :~: (Drop m xs ++ s))
-> (Drop m (xs ++ s) :~: (Drop m xs ++ s))
-> Drop m (xs ++ s) :~: (Drop m xs ++ s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
dropExtensionThm @xs @s PeanoNatural m
m

isLongerOrSameLengthExtThm
  :: forall a s n. IsLongerOrSameLength a n ~ 'True
  => PeanoNatural n
  -> IsLongerOrSameLength (a ++ s) n :~: 'True
isLongerOrSameLengthExtThm :: forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
isLongerOrSameLengthExtThm PeanoNatural n
n = (Stubbed => IsLongerOrSameLength (a ++ s) n :~: 'True)
-> IsLongerOrSameLength (a ++ s) n :~: 'True
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => IsLongerOrSameLength (a ++ s) n :~: 'True)
 -> IsLongerOrSameLength (a ++ s) n :~: 'True)
-> (Stubbed => IsLongerOrSameLength (a ++ s) n :~: 'True)
-> IsLongerOrSameLength (a ++ s) n :~: 'True
forall a b. (a -> b) -> a -> b
$ case PeanoNatural n
n of
  PeanoNatural n
Zero -> 'True :~: 'True
IsLongerOrSameLength (a ++ s) n :~: 'True
forall {k} (a :: k). a :~: a
Refl
  Succ PeanoNatural m
m -> case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
forall {k} (xs :: [k]). KList xs
assumeKnown @a of
    KCons Proxy x
_ (Proxy xs
_ :: Proxy xs) -> 'True :~: 'True
IsLongerOrSameLength (xs ++ s) m :~: 'True
(IsLongerOrSameLength (xs ++ s) m ~ 'True) =>
IsLongerOrSameLength (xs ++ s) m :~: 'True
forall {k} (a :: k). a :~: a
Refl ((IsLongerOrSameLength (xs ++ s) m ~ 'True) =>
 IsLongerOrSameLength (xs ++ s) m :~: 'True)
-> (IsLongerOrSameLength (xs ++ s) m :~: 'True)
-> IsLongerOrSameLength (xs ++ s) m :~: 'True
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
isLongerOrSameLengthExtThm @xs @s PeanoNatural m
m

isLongerOrSameLengthDecThm
  :: forall a m. IsLongerOrSameLength a ('S m) ~ 'True
  => PeanoNatural ('S m)
  -> IsLongerOrSameLength a m :~: 'True
isLongerOrSameLengthDecThm :: forall {k} (a :: [k]) (m :: Peano).
(IsLongerOrSameLength a ('S m) ~ 'True) =>
PeanoNatural ('S m) -> IsLongerOrSameLength a m :~: 'True
isLongerOrSameLengthDecThm PeanoNatural ('S m)
n = (Stubbed => IsLongerOrSameLength a m :~: 'True)
-> IsLongerOrSameLength a m :~: 'True
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => IsLongerOrSameLength a m :~: 'True)
 -> IsLongerOrSameLength a m :~: 'True)
-> (Stubbed => IsLongerOrSameLength a m :~: 'True)
-> IsLongerOrSameLength a m :~: 'True
forall a b. (a -> b) -> a -> b
$ case PeanoNatural ('S m)
n of
  Succ PeanoNatural m
Zero -> 'True :~: 'True
IsLongerOrSameLength a m :~: 'True
forall {k} (a :: k). a :~: a
Refl
  Succ (Succ PeanoNatural m
m) -> case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
forall {k} (xs :: [k]). KList xs
assumeKnown @a of
    KCons Proxy x
_ (Proxy xs
_ :: Proxy xs) -> 'True :~: 'True
IsLongerOrSameLength xs m :~: 'True
(IsLongerOrSameLength xs m ~ 'True) =>
IsLongerOrSameLength xs m :~: 'True
forall {k} (a :: k). a :~: a
Refl ((IsLongerOrSameLength xs m ~ 'True) =>
 IsLongerOrSameLength xs m :~: 'True)
-> (IsLongerOrSameLength xs m :~: 'True)
-> IsLongerOrSameLength xs m :~: 'True
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [k]) (m :: Peano).
(IsLongerOrSameLength a ('S m) ~ 'True) =>
PeanoNatural ('S m) -> IsLongerOrSameLength a m :~: 'True
forall {k} (a :: [k]) (m :: Peano).
(IsLongerOrSameLength a ('S m) ~ 'True) =>
PeanoNatural ('S m) -> IsLongerOrSameLength a m :~: 'True
isLongerOrSameLengthDecThm @xs (PeanoNatural m -> PeanoNatural ('S m)
forall (n :: Peano) (m :: Peano).
(n ~ 'S m) =>
PeanoNatural m -> PeanoNatural n
Succ PeanoNatural m
m)

isLongerThanExtThm
  :: forall a s n. IsLongerThan a n ~ 'True
  => PeanoNatural n
  -> IsLongerThan (a ++ s) n :~: 'True
isLongerThanExtThm :: forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerThan (a ++ s) n :~: 'True
isLongerThanExtThm PeanoNatural n
n = (Stubbed => IsLongerThan (a ++ s) n :~: 'True)
-> IsLongerThan (a ++ s) n :~: 'True
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => IsLongerThan (a ++ s) n :~: 'True)
 -> IsLongerThan (a ++ s) n :~: 'True)
-> (Stubbed => IsLongerThan (a ++ s) n :~: 'True)
-> IsLongerThan (a ++ s) n :~: 'True
forall a b. (a -> b) -> a -> b
$ case PeanoNatural n
n of
  PeanoNatural n
Zero -> case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
forall {k} (xs :: [k]). KList xs
assumeKnown @a of
    KCons{} -> 'True :~: 'True
IsLongerThan (a ++ s) n :~: 'True
forall {k} (a :: k). a :~: a
Refl
  Succ PeanoNatural m
m -> case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
forall {k} (xs :: [k]). KList xs
assumeKnown @a of
    KCons Proxy x
_ (Proxy xs
_ :: Proxy xs) -> 'True :~: 'True
IsLongerThan (xs ++ s) m :~: 'True
(IsLongerThan (xs ++ s) m ~ 'True) =>
IsLongerThan (xs ++ s) m :~: 'True
forall {k} (a :: k). a :~: a
Refl ((IsLongerThan (xs ++ s) m ~ 'True) =>
 IsLongerThan (xs ++ s) m :~: 'True)
-> (IsLongerThan (xs ++ s) m :~: 'True)
-> IsLongerThan (xs ++ s) m :~: 'True
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerThan (a ++ s) n :~: 'True
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerThan (a ++ s) n :~: 'True
isLongerThanExtThm @xs @s PeanoNatural m
m

dropHeadThm
  :: forall x a n. IsLongerThan (x : a) n ~ 'True
  => PeanoNatural n
  -> IsLongerOrSameLength a n :~: 'True
dropHeadThm :: forall {k} (x :: k) (a :: [k]) (n :: Peano).
(IsLongerThan (x : a) n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a n :~: 'True
dropHeadThm PeanoNatural n
n = (Stubbed => IsLongerOrSameLength a n :~: 'True)
-> IsLongerOrSameLength a n :~: 'True
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => IsLongerOrSameLength a n :~: 'True)
 -> IsLongerOrSameLength a n :~: 'True)
-> (Stubbed => IsLongerOrSameLength a n :~: 'True)
-> IsLongerOrSameLength a n :~: 'True
forall a b. (a -> b) -> a -> b
$ case PeanoNatural n
n of
  PeanoNatural n
Zero -> 'True :~: 'True
IsLongerOrSameLength a n :~: 'True
forall {k} (a :: k). a :~: a
Refl
  Succ PeanoNatural m
m -> case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
forall {k} (xs :: [k]). KList xs
assumeKnown @a of
    KCons (Proxy x
_ :: Proxy y) (Proxy xs
_ :: Proxy xs) -> 'True :~: 'True
IsLongerOrSameLength xs m :~: 'True
(IsLongerOrSameLength xs m ~ 'True) =>
IsLongerOrSameLength xs m :~: 'True
forall {k} (a :: k). a :~: a
Refl ((IsLongerOrSameLength xs m ~ 'True) =>
 IsLongerOrSameLength xs m :~: 'True)
-> (IsLongerOrSameLength xs m :~: 'True)
-> IsLongerOrSameLength xs m :~: 'True
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (x :: k) (a :: [k]) (n :: Peano).
(IsLongerThan (x : a) n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a n :~: 'True
forall {k} (x :: k) (a :: [k]) (n :: Peano).
(IsLongerThan (x : a) n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a n :~: 'True
dropHeadThm @y @xs PeanoNatural m
m

isLongerThanIncThm
  :: forall a n. IsLongerThan a n ~ 'True
  => PeanoNatural n
  -> IsLongerOrSameLength a ('S n) :~: 'True
isLongerThanIncThm :: forall {k} (a :: [k]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a ('S n) :~: 'True
isLongerThanIncThm PeanoNatural n
n = (Stubbed => IsLongerOrSameLength a ('S n) :~: 'True)
-> IsLongerOrSameLength a ('S n) :~: 'True
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => IsLongerOrSameLength a ('S n) :~: 'True)
 -> IsLongerOrSameLength a ('S n) :~: 'True)
-> (Stubbed => IsLongerOrSameLength a ('S n) :~: 'True)
-> IsLongerOrSameLength a ('S n) :~: 'True
forall a b. (a -> b) -> a -> b
$ case PeanoNatural n
n of
  PeanoNatural n
Zero -> case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
forall {k} (xs :: [k]). KList xs
assumeKnown @a of
    KCons{} -> 'True :~: 'True
IsLongerOrSameLength a ('S n) :~: 'True
forall {k} (a :: k). a :~: a
Refl
  Succ PeanoNatural m
m -> case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
forall {k} (xs :: [k]). KList xs
assumeKnown @a of
    KCons Proxy x
_ (Proxy xs
_ :: Proxy xs) -> 'True :~: 'True
IsLongerOrSameLength xs ('S m) :~: 'True
(IsLongerOrSameLength xs ('S m) ~ 'True) =>
IsLongerOrSameLength xs ('S m) :~: 'True
forall {k} (a :: k). a :~: a
Refl ((IsLongerOrSameLength xs ('S m) ~ 'True) =>
 IsLongerOrSameLength xs ('S m) :~: 'True)
-> (IsLongerOrSameLength xs ('S m) :~: 'True)
-> IsLongerOrSameLength xs ('S m) :~: 'True
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [k]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a ('S n) :~: 'True
forall {k} (a :: [k]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a ('S n) :~: 'True
isLongerThanIncThm @xs PeanoNatural m
m

dugLengthThm
  :: forall b x n. IsLongerThan b n ~ 'True
  => PeanoNatural n
  -> IsLongerThan (x ': LazyTake n b ++ Drop ('S n) b) n :~: 'True
dugLengthThm :: forall {k} (b :: [k]) (x :: k) (n :: Peano).
(IsLongerThan b n ~ 'True) =>
PeanoNatural n
-> IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True
dugLengthThm PeanoNatural n
n = (Stubbed =>
 IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True)
-> IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed =>
  IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True)
 -> IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True)
-> (Stubbed =>
    IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True)
-> IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True
forall a b. (a -> b) -> a -> b
$ case PeanoNatural n
n of
  PeanoNatural n
Zero -> 'True :~: 'True
IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True
forall {k} (a :: k). a :~: a
Refl
  Succ PeanoNatural m
m -> case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
forall {k} (xs :: [k]). KList xs
assumeKnown @b of
    KCons (Proxy x
_ :: Proxy y) (Proxy xs
_ :: Proxy xs) -> 'True :~: 'True
IsLongerThan (x : (LazyTake m xs ++ Drop ('S m) xs)) m :~: 'True
(IsLongerThan (x : (LazyTake m xs ++ Drop ('S m) xs)) m ~ 'True) =>
IsLongerThan (x : (LazyTake m xs ++ Drop ('S m) xs)) m :~: 'True
forall {k} (a :: k). a :~: a
Refl ((IsLongerThan (x : (LazyTake m xs ++ Drop ('S m) xs)) m
  ~ 'True) =>
 IsLongerThan (x : (LazyTake m xs ++ Drop ('S m) xs)) m :~: 'True)
-> (IsLongerThan (x : (LazyTake m xs ++ Drop ('S m) xs)) m
    :~: 'True)
-> IsLongerThan (x : (LazyTake m xs ++ Drop ('S m) xs)) m :~: 'True
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (b :: [k]) (x :: k) (n :: Peano).
(IsLongerThan b n ~ 'True) =>
PeanoNatural n
-> IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True
forall {k} (b :: [k]) (x :: k) (n :: Peano).
(IsLongerThan b n ~ 'True) =>
PeanoNatural n
-> IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True
dugLengthThm @xs @y PeanoNatural m
m

dropNExtensionThm
  :: forall s a b n. (Drop n a ~ b, IsLongerOrSameLength a n ~ 'True)
  => PeanoNatural n
  -> Dict (Drop n (a ++ s) ~ b ++ s, IsLongerOrSameLength (a ++ s) n ~ 'True)
dropNExtensionThm :: forall {k} (s :: [k]) (a :: [k]) (b :: [k]) (n :: Peano).
(Drop n a ~ b, IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n
-> Dict
     (Drop n (a ++ s) ~ (b ++ s),
      IsLongerOrSameLength (a ++ s) n ~ 'True)
dropNExtensionThm PeanoNatural n
n = Dict ((b ++ s) ~ (b ++ s), 'True ~ 'True)
Dict
  (Drop n (a ++ s) ~ (b ++ s),
   IsLongerOrSameLength (a ++ s) n ~ 'True)
(Drop n (a ++ s) ~ (b ++ s)) =>
Dict
  (Drop n (a ++ s) ~ (b ++ s),
   IsLongerOrSameLength (a ++ s) n ~ 'True)
forall (a :: Constraint). a => Dict a
Dict
  ((Drop n (a ++ s) ~ (b ++ s)) =>
 Dict
   (Drop n (a ++ s) ~ (b ++ s),
    IsLongerOrSameLength (a ++ s) n ~ 'True))
-> (Drop n (a ++ s) :~: (b ++ s))
-> Dict
     (Drop n (a ++ s) ~ (b ++ s),
      IsLongerOrSameLength (a ++ s) n ~ 'True)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
dropExtensionThm @a @s PeanoNatural n
n
  ((IsLongerOrSameLength (a ++ s) n ~ 'True) =>
 Dict
   (Drop n (a ++ s) ~ (b ++ s),
    IsLongerOrSameLength (a ++ s) n ~ 'True))
-> (IsLongerOrSameLength (a ++ s) n :~: 'True)
-> Dict
     (Drop n (a ++ s) ~ (b ++ s),
      IsLongerOrSameLength (a ++ s) n ~ 'True)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
isLongerOrSameLengthExtThm @a @s PeanoNatural n
n

dupNExtensionThm
  :: forall s a b n x. (ConstraintDUPN n a b x)
  => PeanoNatural n
  -> Dict (ConstraintDUPN n (a ++ s) (b ++ s) x)
dupNExtensionThm :: forall (s :: [T]) (a :: [T]) (b :: [T]) (n :: Peano) (x :: T).
ConstraintDUPN n a b x =>
PeanoNatural n -> Dict (ConstraintDUPN n (a ++ s) (b ++ s) x)
dupNExtensionThm n :: PeanoNatural n
n@(Succ PeanoNatural m
m) = Dict
  (RequireLongerOrSameLength (a ++ s) ('S m), 'True ~ 'True,
   (a ++ s) ~ (LazyTake m (a ++ s) ++ (x : Drop ('S m) (a ++ s))),
   (x : (a ++ s)) ~ (x : (a ++ s)))
Dict
  (RequireLongerOrSameLength
     (LazyTake m a ++ (x : (Drop ('S m) a ++ s))) ('S m),
   'True ~ 'True,
   (LazyTake m a ++ (x : (Drop ('S m) a ++ s)))
   ~ (LazyTake m a ++ (x : (Drop ('S m) a ++ s))),
   (x : (LazyTake m a ++ (x : (Drop ('S m) a ++ s))))
   ~ (x : (LazyTake m a ++ (x : (Drop ('S m) a ++ s)))))
(IsLongerOrSameLength
   (LazyTake m a ++ (x : (Drop ('S m) a ++ s))) ('S m)
 ~ 'True) =>
Dict
  (RequireLongerOrSameLength (a ++ s) ('S m), 'True ~ 'True,
   (a ++ s) ~ (LazyTake m (a ++ s) ++ (x : Drop ('S m) (a ++ s))),
   (x : (a ++ s)) ~ (x : (a ++ s)))
forall (a :: Constraint). a => Dict a
Dict
  ((IsLongerOrSameLength
    (LazyTake m a ++ (x : (Drop ('S m) a ++ s))) ('S m)
  ~ 'True) =>
 Dict
   (RequireLongerOrSameLength (a ++ s) ('S m), 'True ~ 'True,
    (a ++ s) ~ (LazyTake m (a ++ s) ++ (x : Drop ('S m) (a ++ s))),
    (x : (a ++ s)) ~ (x : (a ++ s))))
-> (IsLongerOrSameLength
      (LazyTake m a ++ (x : (Drop ('S m) a ++ s))) ('S m)
    :~: 'True)
-> Dict
     (RequireLongerOrSameLength (a ++ s) ('S m), 'True ~ 'True,
      (a ++ s) ~ (LazyTake m (a ++ s) ++ (x : Drop ('S m) (a ++ s))),
      (x : (a ++ s)) ~ (x : (a ++ s)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
isLongerOrSameLengthExtThm @a @s PeanoNatural n
n
  (((a ++ s) ~ (LazyTake m a ++ (x : (Drop ('S m) a ++ s)))) =>
 Dict
   (RequireLongerOrSameLength (a ++ s) ('S m), 'True ~ 'True,
    (a ++ s) ~ (LazyTake m (a ++ s) ++ (x : Drop ('S m) (a ++ s))),
    (x : (a ++ s)) ~ (x : (a ++ s))))
-> ((a ++ s) :~: (LazyTake m a ++ (x : (Drop ('S m) a ++ s))))
-> Dict
     (RequireLongerOrSameLength (a ++ s) ('S m), 'True ~ 'True,
      (a ++ s) ~ (LazyTake m (a ++ s) ++ (x : Drop ('S m) (a ++ s))),
      (x : (a ++ s)) ~ (x : (a ++ s)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (b :: [T]) (c :: [T]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall {k} (a :: [k]) (b :: [k]) (c :: [k]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
assocThm @(LazyTake (Decrement n) a) @(x : Drop n a) @s
  ((LazyTake m (a ++ s) ~ LazyTake m a) =>
 Dict
   (RequireLongerOrSameLength (a ++ s) ('S m), 'True ~ 'True,
    (a ++ s) ~ (LazyTake m (a ++ s) ++ (x : Drop ('S m) (a ++ s))),
    (x : (a ++ s)) ~ (x : (a ++ s))))
-> (LazyTake m (a ++ s) :~: LazyTake m a)
-> Dict
     (RequireLongerOrSameLength (a ++ s) ('S m), 'True ~ 'True,
      (a ++ s) ~ (LazyTake m (a ++ s) ++ (x : Drop ('S m) (a ++ s))),
      (x : (a ++ s)) ~ (x : (a ++ s)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
takeExtensionThm @a @s PeanoNatural m
m ((IsLongerOrSameLength a m ~ 'True) =>
 Dict
   (RequireLongerOrSameLength (a ++ s) ('S m), 'True ~ 'True,
    (a ++ s) ~ (LazyTake m (a ++ s) ++ (x : Drop ('S m) (a ++ s))),
    (x : (a ++ s)) ~ (x : (a ++ s))))
-> (IsLongerOrSameLength a m :~: 'True)
-> Dict
     (RequireLongerOrSameLength (a ++ s) ('S m), 'True ~ 'True,
      (a ++ s) ~ (LazyTake m (a ++ s) ++ (x : Drop ('S m) (a ++ s))),
      (x : (a ++ s)) ~ (x : (a ++ s)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (m :: Peano).
(IsLongerOrSameLength a ('S m) ~ 'True) =>
PeanoNatural ('S m) -> IsLongerOrSameLength a m :~: 'True
forall {k} (a :: [k]) (m :: Peano).
(IsLongerOrSameLength a ('S m) ~ 'True) =>
PeanoNatural ('S m) -> IsLongerOrSameLength a m :~: 'True
isLongerOrSameLengthDecThm @a PeanoNatural n
PeanoNatural ('S m)
n
  ((Drop ('S m) (a ++ s) ~ (Drop ('S m) a ++ s)) =>
 Dict
   (RequireLongerOrSameLength (a ++ s) ('S m), 'True ~ 'True,
    (a ++ s) ~ (LazyTake m (a ++ s) ++ (x : Drop ('S m) (a ++ s))),
    (x : (a ++ s)) ~ (x : (a ++ s))))
-> (Drop ('S m) (a ++ s) :~: (Drop ('S m) a ++ s))
-> Dict
     (RequireLongerOrSameLength (a ++ s) ('S m), 'True ~ 'True,
      (a ++ s) ~ (LazyTake m (a ++ s) ++ (x : Drop ('S m) (a ++ s))),
      (x : (a ++ s)) ~ (x : (a ++ s)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
dropExtensionThm @a @s PeanoNatural n
n

dugNExtensionThm
  :: forall s a b x r n. (a ~ x : r, ConstraintDUG n a b x)
  => PeanoNatural n
  -> Dict (ConstraintDUG n (a ++ s) (b ++ s) x)
dugNExtensionThm :: forall (s :: [T]) (a :: [T]) (b :: [T]) (x :: T) (r :: [T])
       (n :: Peano).
(a ~ (x : r), ConstraintDUG n a b x) =>
PeanoNatural n -> Dict (ConstraintDUG n (a ++ s) (b ++ s) x)
dugNExtensionThm PeanoNatural n
n = Dict
  (RequireLongerThan (b ++ s) n,
   (x : (r ++ s))
   ~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
   (b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
Dict
  (RequireLongerThan (LazyTake n r ++ (x : (Drop n r ++ s))) n,
   (x : (LazyTake n b ++ (Drop ('S n) b ++ s)))
   ~ (x : (LazyTake n b ++ (Drop ('S n) b ++ s))),
   (LazyTake n r ++ (x : (Drop n r ++ s)))
   ~ (LazyTake n r ++ (x : (Drop n r ++ s))))
(IsLongerThan (LazyTake n r ++ (x : (Drop n r ++ s))) n ~ 'True) =>
Dict
  (RequireLongerThan (b ++ s) n,
   (x : (r ++ s))
   ~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
   (b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (a :: Constraint). a => Dict a
Dict
  ((IsLongerThan (LazyTake n r ++ (x : (Drop n r ++ s))) n
  ~ 'True) =>
 Dict
   (RequireLongerThan (b ++ s) n,
    (x : (r ++ s))
    ~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
    (b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (IsLongerThan (LazyTake n r ++ (x : (Drop n r ++ s))) n
    :~: 'True)
-> Dict
     (RequireLongerThan (b ++ s) n,
      (x : (r ++ s))
      ~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
      (b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerThan (a ++ s) n :~: 'True
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerThan (a ++ s) n :~: 'True
isLongerThanExtThm @b @s PeanoNatural n
n
  (((r ++ s) ~ (LazyTake n b ++ (Drop ('S n) b ++ s))) =>
 Dict
   (RequireLongerThan (b ++ s) n,
    (x : (r ++ s))
    ~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
    (b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> ((r ++ s) :~: (LazyTake n b ++ (Drop ('S n) b ++ s)))
-> Dict
     (RequireLongerThan (b ++ s) n,
      (x : (r ++ s))
      ~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
      (b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (b :: [T]) (c :: [T]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall {k} (a :: [k]) (b :: [k]) (c :: [k]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
assocThm @(LazyTake n b) @(Drop ('S n) b) @s
  ((LazyTake n (LazyTake n r ++ (x : (Drop n r ++ s)))
  ~ LazyTake n b) =>
 Dict
   (RequireLongerThan (b ++ s) n,
    (x : (r ++ s))
    ~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
    (b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (LazyTake n (LazyTake n r ++ (x : (Drop n r ++ s)))
    :~: LazyTake n b)
-> Dict
     (RequireLongerThan (b ++ s) n,
      (x : (r ++ s))
      ~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
      (b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
takeExtensionThm @b @s PeanoNatural n
n ((IsLongerOrSameLength b n ~ 'True) =>
 Dict
   (RequireLongerThan (b ++ s) n,
    (x : (r ++ s))
    ~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
    (b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (IsLongerOrSameLength b n :~: 'True)
-> Dict
     (RequireLongerThan (b ++ s) n,
      (x : (r ++ s))
      ~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
      (b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (m :: Peano).
(IsLongerOrSameLength a ('S m) ~ 'True) =>
PeanoNatural ('S m) -> IsLongerOrSameLength a m :~: 'True
forall {k} (a :: [k]) (m :: Peano).
(IsLongerOrSameLength a ('S m) ~ 'True) =>
PeanoNatural ('S m) -> IsLongerOrSameLength a m :~: 'True
isLongerOrSameLengthDecThm @b (PeanoNatural n -> PeanoNatural ('S n)
forall (n :: Peano) (m :: Peano).
(n ~ 'S m) =>
PeanoNatural m -> PeanoNatural n
Succ PeanoNatural n
n)
  ((Drop ('S n) (LazyTake n r ++ (x : (Drop n r ++ s)))
  ~ (Drop ('S n) b ++ s)) =>
 Dict
   (RequireLongerThan (b ++ s) n,
    (x : (r ++ s))
    ~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
    (b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (Drop ('S n) (LazyTake n r ++ (x : (Drop n r ++ s)))
    :~: (Drop ('S n) b ++ s))
-> Dict
     (RequireLongerThan (b ++ s) n,
      (x : (r ++ s))
      ~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
      (b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
dropExtensionThm @b @s (PeanoNatural n -> PeanoNatural ('S n)
forall (n :: Peano) (m :: Peano).
(n ~ 'S m) =>
PeanoNatural m -> PeanoNatural n
Succ PeanoNatural n
n)
  ((IsLongerOrSameLength b ('S n) ~ 'True) =>
 Dict
   (RequireLongerThan (b ++ s) n,
    (x : (r ++ s))
    ~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
    (b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (IsLongerOrSameLength b ('S n) :~: 'True)
-> Dict
     (RequireLongerThan (b ++ s) n,
      (x : (r ++ s))
      ~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
      (b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a ('S n) :~: 'True
forall {k} (a :: [k]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a ('S n) :~: 'True
isLongerThanIncThm @b PeanoNatural n
n
  (((b ++ s) ~ (LazyTake n r ++ (x : (Drop n r ++ s)))) =>
 Dict
   (RequireLongerThan (b ++ s) n,
    (x : (r ++ s))
    ~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
    (b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> ((b ++ s) :~: (LazyTake n r ++ (x : (Drop n r ++ s))))
-> Dict
     (RequireLongerThan (b ++ s) n,
      (x : (r ++ s))
      ~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
      (b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (b :: [T]) (c :: [T]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall {k} (a :: [k]) (b :: [k]) (c :: [k]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
assocThm @(LazyTake n r) @(x : Drop n r) @s
  ((LazyTake n (r ++ s) ~ LazyTake n r) =>
 Dict
   (RequireLongerThan (b ++ s) n,
    (x : (r ++ s))
    ~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
    (b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (LazyTake n (r ++ s) :~: LazyTake n r)
-> Dict
     (RequireLongerThan (b ++ s) n,
      (x : (r ++ s))
      ~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
      (b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
takeExtensionThm @r @s PeanoNatural n
n ((Drop n (r ++ s) ~ (Drop n r ++ s)) =>
 Dict
   (RequireLongerThan (b ++ s) n,
    (x : (r ++ s))
    ~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
    (b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (Drop n (r ++ s) :~: (Drop n r ++ s))
-> Dict
     (RequireLongerThan (b ++ s) n,
      (x : (r ++ s))
      ~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
      (b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
dropExtensionThm @r @s PeanoNatural n
n ((IsLongerOrSameLength r n ~ 'True) =>
 Dict
   (RequireLongerThan (b ++ s) n,
    (x : (r ++ s))
    ~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
    (b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (IsLongerOrSameLength r n :~: 'True)
-> Dict
     (RequireLongerThan (b ++ s) n,
      (x : (r ++ s))
      ~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
      (b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall {k} (x :: k) (a :: [k]) (n :: Peano).
(IsLongerThan (x : a) n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a n :~: 'True
forall (x :: T) (a :: [T]) (n :: Peano).
(IsLongerThan (x : a) n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a n :~: 'True
dropHeadThm @x @r PeanoNatural n
n
  ((IsLongerThan (x : r) n ~ 'True) =>
 Dict
   (RequireLongerThan (b ++ s) n,
    (x : (r ++ s))
    ~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
    (b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (IsLongerThan (x : r) n :~: 'True)
-> Dict
     (RequireLongerThan (b ++ s) n,
      (x : (r ++ s))
      ~ (x : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
      (b ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (b :: [T]) (x :: T) (n :: Peano).
(IsLongerThan b n ~ 'True) =>
PeanoNatural n
-> IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True
forall {k} (b :: [k]) (x :: k) (n :: Peano).
(IsLongerThan b n ~ 'True) =>
PeanoNatural n
-> IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True
dugLengthThm @b @x PeanoNatural n
n

digNExtensionThm
  :: forall s a b x r n. (b ~ x : r, ConstraintDIG n a b x)
  => PeanoNatural n
  -> Dict (ConstraintDIG n (a ++ s) (b ++ s) x)
digNExtensionThm :: forall (s :: [T]) (a :: [T]) (b :: [T]) (x :: T) (r :: [T])
       (n :: Peano).
(b ~ (x : r), ConstraintDIG n a b x) =>
PeanoNatural n -> Dict (ConstraintDIG n (a ++ s) (b ++ s) x)
digNExtensionThm PeanoNatural n
n = Dict
  (RequireLongerThan (a ++ s) n,
   (x : (r ++ s))
   ~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
   (a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
Dict
  (RequireLongerThan (LazyTake n r ++ (x : (Drop n r ++ s))) n,
   (x : (LazyTake n a ++ (Drop ('S n) a ++ s)))
   ~ (x : (LazyTake n a ++ (Drop ('S n) a ++ s))),
   (LazyTake n r ++ (x : (Drop n r ++ s)))
   ~ (LazyTake n r ++ (x : (Drop n r ++ s))))
(IsLongerThan (LazyTake n r ++ (x : (Drop n r ++ s))) n ~ 'True) =>
Dict
  (RequireLongerThan (a ++ s) n,
   (x : (r ++ s))
   ~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
   (a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (a :: Constraint). a => Dict a
Dict
  ((IsLongerThan (LazyTake n r ++ (x : (Drop n r ++ s))) n
  ~ 'True) =>
 Dict
   (RequireLongerThan (a ++ s) n,
    (x : (r ++ s))
    ~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
    (a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (IsLongerThan (LazyTake n r ++ (x : (Drop n r ++ s))) n
    :~: 'True)
-> Dict
     (RequireLongerThan (a ++ s) n,
      (x : (r ++ s))
      ~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
      (a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerThan (a ++ s) n :~: 'True
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerThan (a ++ s) n :~: 'True
isLongerThanExtThm @a @s PeanoNatural n
n
  (((r ++ s) ~ (LazyTake n a ++ (Drop ('S n) a ++ s))) =>
 Dict
   (RequireLongerThan (a ++ s) n,
    (x : (r ++ s))
    ~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
    (a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> ((r ++ s) :~: (LazyTake n a ++ (Drop ('S n) a ++ s)))
-> Dict
     (RequireLongerThan (a ++ s) n,
      (x : (r ++ s))
      ~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
      (a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (b :: [T]) (c :: [T]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall {k} (a :: [k]) (b :: [k]) (c :: [k]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
assocThm @(LazyTake n a) @(Drop ('S n) a) @s
  ((LazyTake n (LazyTake n r ++ (x : (Drop n r ++ s)))
  ~ LazyTake n a) =>
 Dict
   (RequireLongerThan (a ++ s) n,
    (x : (r ++ s))
    ~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
    (a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (LazyTake n (LazyTake n r ++ (x : (Drop n r ++ s)))
    :~: LazyTake n a)
-> Dict
     (RequireLongerThan (a ++ s) n,
      (x : (r ++ s))
      ~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
      (a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
takeExtensionThm @a @s PeanoNatural n
n ((IsLongerOrSameLength a n ~ 'True) =>
 Dict
   (RequireLongerThan (a ++ s) n,
    (x : (r ++ s))
    ~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
    (a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (IsLongerOrSameLength a n :~: 'True)
-> Dict
     (RequireLongerThan (a ++ s) n,
      (x : (r ++ s))
      ~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
      (a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (m :: Peano).
(IsLongerOrSameLength a ('S m) ~ 'True) =>
PeanoNatural ('S m) -> IsLongerOrSameLength a m :~: 'True
forall {k} (a :: [k]) (m :: Peano).
(IsLongerOrSameLength a ('S m) ~ 'True) =>
PeanoNatural ('S m) -> IsLongerOrSameLength a m :~: 'True
isLongerOrSameLengthDecThm @a (PeanoNatural n -> PeanoNatural ('S n)
forall (n :: Peano) (m :: Peano).
(n ~ 'S m) =>
PeanoNatural m -> PeanoNatural n
Succ PeanoNatural n
n)
  ((Drop ('S n) (LazyTake n r ++ (x : (Drop n r ++ s)))
  ~ (Drop ('S n) a ++ s)) =>
 Dict
   (RequireLongerThan (a ++ s) n,
    (x : (r ++ s))
    ~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
    (a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (Drop ('S n) (LazyTake n r ++ (x : (Drop n r ++ s)))
    :~: (Drop ('S n) a ++ s))
-> Dict
     (RequireLongerThan (a ++ s) n,
      (x : (r ++ s))
      ~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
      (a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
dropExtensionThm @a @s (PeanoNatural n -> PeanoNatural ('S n)
forall (n :: Peano) (m :: Peano).
(n ~ 'S m) =>
PeanoNatural m -> PeanoNatural n
Succ PeanoNatural n
n)
  ((IsLongerOrSameLength a ('S n) ~ 'True) =>
 Dict
   (RequireLongerThan (a ++ s) n,
    (x : (r ++ s))
    ~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
    (a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (IsLongerOrSameLength a ('S n) :~: 'True)
-> Dict
     (RequireLongerThan (a ++ s) n,
      (x : (r ++ s))
      ~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
      (a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a ('S n) :~: 'True
forall {k} (a :: [k]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a ('S n) :~: 'True
isLongerThanIncThm @a PeanoNatural n
n
  (((a ++ s) ~ (LazyTake n r ++ (x : (Drop n r ++ s)))) =>
 Dict
   (RequireLongerThan (a ++ s) n,
    (x : (r ++ s))
    ~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
    (a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> ((a ++ s) :~: (LazyTake n r ++ (x : (Drop n r ++ s))))
-> Dict
     (RequireLongerThan (a ++ s) n,
      (x : (r ++ s))
      ~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
      (a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (b :: [T]) (c :: [T]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall {k} (a :: [k]) (b :: [k]) (c :: [k]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
assocThm @(LazyTake n r) @(x : Drop n r) @s
  ((LazyTake n (r ++ s) ~ LazyTake n r) =>
 Dict
   (RequireLongerThan (a ++ s) n,
    (x : (r ++ s))
    ~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
    (a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (LazyTake n (r ++ s) :~: LazyTake n r)
-> Dict
     (RequireLongerThan (a ++ s) n,
      (x : (r ++ s))
      ~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
      (a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
takeExtensionThm @r @s PeanoNatural n
n ((Drop n (r ++ s) ~ (Drop n r ++ s)) =>
 Dict
   (RequireLongerThan (a ++ s) n,
    (x : (r ++ s))
    ~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
    (a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (Drop n (r ++ s) :~: (Drop n r ++ s))
-> Dict
     (RequireLongerThan (a ++ s) n,
      (x : (r ++ s))
      ~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
      (a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
dropExtensionThm @r @s PeanoNatural n
n ((IsLongerOrSameLength r n ~ 'True) =>
 Dict
   (RequireLongerThan (a ++ s) n,
    (x : (r ++ s))
    ~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
    (a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (IsLongerOrSameLength r n :~: 'True)
-> Dict
     (RequireLongerThan (a ++ s) n,
      (x : (r ++ s))
      ~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
      (a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall {k} (x :: k) (a :: [k]) (n :: Peano).
(IsLongerThan (x : a) n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a n :~: 'True
forall (x :: T) (a :: [T]) (n :: Peano).
(IsLongerThan (x : a) n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength a n :~: 'True
dropHeadThm @x @r PeanoNatural n
n
  ((IsLongerThan (x : r) n ~ 'True) =>
 Dict
   (RequireLongerThan (a ++ s) n,
    (x : (r ++ s))
    ~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
    (a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s)))))
-> (IsLongerThan (x : r) n :~: 'True)
-> Dict
     (RequireLongerThan (a ++ s) n,
      (x : (r ++ s))
      ~ (x : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
      (a ++ s) ~ (LazyTake n (r ++ s) ++ (x : Drop n (r ++ s))))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (b :: [T]) (x :: T) (n :: Peano).
(IsLongerThan b n ~ 'True) =>
PeanoNatural n
-> IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True
forall {k} (b :: [k]) (x :: k) (n :: Peano).
(IsLongerThan b n ~ 'True) =>
PeanoNatural n
-> IsLongerThan (x : (LazyTake n b ++ Drop ('S n) b)) n :~: 'True
dugLengthThm @a @x PeanoNatural n
n

dipNExtensionThm
  :: forall s a b s1 s1' n. ConstraintDIPN n a b s1 s1'
  => PeanoNatural n
  -> Dict (ConstraintDIPN n (a ++ s) (b ++ s) (s1 ++ s) (s1' ++ s))
dipNExtensionThm :: forall (s :: [T]) (a :: [T]) (b :: [T]) (s1 :: [T]) (s1' :: [T])
       (n :: Peano).
ConstraintDIPN n a b s1 s1' =>
PeanoNatural n
-> Dict (ConstraintDIPN n (a ++ s) (b ++ s) (s1 ++ s) (s1' ++ s))
dipNExtensionThm PeanoNatural n
n = Dict
  (RequireLongerOrSameLength (a ++ s) n,
   (LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
   (LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
   (s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s))
Dict
  (RequireLongerOrSameLength (LazyTake n a ++ (s1 ++ s)) n,
   (LazyTake n a ++ (s1 ++ s)) ~ (LazyTake n a ++ (s1 ++ s)),
   (LazyTake n a ++ (s1' ++ s)) ~ (LazyTake n a ++ (s1' ++ s)),
   (s1 ++ s) ~ (s1 ++ s), (s1' ++ s) ~ (s1' ++ s))
(IsLongerOrSameLength (LazyTake n a ++ (s1 ++ s)) n ~ 'True) =>
Dict
  (RequireLongerOrSameLength (a ++ s) n,
   (LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
   (LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
   (s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s))
forall (a :: Constraint). a => Dict a
Dict
  ((IsLongerOrSameLength (LazyTake n a ++ (s1 ++ s)) n ~ 'True) =>
 Dict
   (RequireLongerOrSameLength (a ++ s) n,
    (LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
    (LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
    (s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s)))
-> (IsLongerOrSameLength (LazyTake n a ++ (s1 ++ s)) n :~: 'True)
-> Dict
     (RequireLongerOrSameLength (a ++ s) n,
      (LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
      (LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
      (s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
isLongerOrSameLengthExtThm @a @s PeanoNatural n
n
  ((Drop n (LazyTake n a ++ (s1 ++ s)) ~ (s1 ++ s)) =>
 Dict
   (RequireLongerOrSameLength (a ++ s) n,
    (LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
    (LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
    (s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s)))
-> (Drop n (LazyTake n a ++ (s1 ++ s)) :~: (s1 ++ s))
-> Dict
     (RequireLongerOrSameLength (a ++ s) n,
      (LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
      (LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
      (s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
dropExtensionThm @a @s PeanoNatural n
n
  (((b ++ s) ~ (LazyTake n a ++ (s1' ++ s))) =>
 Dict
   (RequireLongerOrSameLength (a ++ s) n,
    (LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
    (LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
    (s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s)))
-> ((b ++ s) :~: (LazyTake n a ++ (s1' ++ s)))
-> Dict
     (RequireLongerOrSameLength (a ++ s) n,
      (LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
      (LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
      (s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (b :: [T]) (c :: [T]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall {k} (a :: [k]) (b :: [k]) (c :: [k]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
assocThm @(LazyTake n a) @s1' @s
  ((LazyTake n (LazyTake n a ++ (s1 ++ s)) ~ LazyTake n a) =>
 Dict
   (RequireLongerOrSameLength (a ++ s) n,
    (LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
    (LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
    (s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s)))
-> (LazyTake n (LazyTake n a ++ (s1 ++ s)) :~: LazyTake n a)
-> Dict
     (RequireLongerOrSameLength (a ++ s) n,
      (LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
      (LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
      (s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
takeExtensionThm @a @s PeanoNatural n
n
  (((a ++ s) ~ (LazyTake n a ++ (s1 ++ s))) =>
 Dict
   (RequireLongerOrSameLength (a ++ s) n,
    (LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
    (LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
    (s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s)))
-> ((a ++ s) :~: (LazyTake n a ++ (s1 ++ s)))
-> Dict
     (RequireLongerOrSameLength (a ++ s) n,
      (LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
      (LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
      (s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (b :: [T]) (c :: [T]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall {k} (a :: [k]) (b :: [k]) (c :: [k]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
assocThm @(LazyTake n a) @s1 @s
  ((Drop n (b ++ s) ~ (s1' ++ s)) =>
 Dict
   (RequireLongerOrSameLength (a ++ s) n,
    (LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
    (LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
    (s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s)))
-> (Drop n (b ++ s) :~: (s1' ++ s))
-> Dict
     (RequireLongerOrSameLength (a ++ s) n,
      (LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
      (LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
      (s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
dropExtensionThm @b @s PeanoNatural n
n
  ((IsLongerOrSameLength (b ++ s) n ~ 'True) =>
 Dict
   (RequireLongerOrSameLength (a ++ s) n,
    (LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
    (LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
    (s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s)))
-> (IsLongerOrSameLength (b ++ s) n :~: 'True)
-> Dict
     (RequireLongerOrSameLength (a ++ s) n,
      (LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
      (LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
      (s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
isLongerOrSameLengthExtThm @b @s PeanoNatural n
n
  ((IsLongerOrSameLength b n ~ 'True) =>
 Dict
   (RequireLongerOrSameLength (a ++ s) n,
    (LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
    (LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
    (s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s)))
-> (IsLongerOrSameLength b n :~: 'True)
-> Dict
     (RequireLongerOrSameLength (a ++ s) n,
      (LazyTake n (a ++ s) ++ (s1 ++ s)) ~ (a ++ s),
      (LazyTake n (a ++ s) ++ (s1' ++ s)) ~ (b ++ s),
      (s1 ++ s) ~ Drop n (a ++ s), (s1' ++ s) ~ Drop n (b ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (inp :: [T]) (out :: [T]) (s :: [T]) (n :: Peano).
(RequireLongerOrSameLength inp n, (LazyTake n inp ++ s) ~ out) =>
PeanoNatural n -> IsLongerOrSameLength out n :~: 'True
forall {k} (inp :: [k]) (out :: [k]) (s :: [k]) (n :: Peano).
(RequireLongerOrSameLength inp n, (LazyTake n inp ++ s) ~ out) =>
PeanoNatural n -> IsLongerOrSameLength out n :~: 'True
dipNExtensionLemma @a @b @s1' PeanoNatural n
n

dipNExtensionLemma ::
  forall inp out s n.
    ( RequireLongerOrSameLength inp n
    , LazyTake n inp ++ s ~ out)
  => PeanoNatural n
  -> IsLongerOrSameLength out n :~: 'True
dipNExtensionLemma :: forall {k} (inp :: [k]) (out :: [k]) (s :: [k]) (n :: Peano).
(RequireLongerOrSameLength inp n, (LazyTake n inp ++ s) ~ out) =>
PeanoNatural n -> IsLongerOrSameLength out n :~: 'True
dipNExtensionLemma PeanoNatural n
n = (Stubbed => IsLongerOrSameLength out n :~: 'True)
-> IsLongerOrSameLength out n :~: 'True
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof ((Stubbed => IsLongerOrSameLength out n :~: 'True)
 -> IsLongerOrSameLength out n :~: 'True)
-> (Stubbed => IsLongerOrSameLength out n :~: 'True)
-> IsLongerOrSameLength out n :~: 'True
forall a b. (a -> b) -> a -> b
$ case PeanoNatural n
n of
  PeanoNatural n
Zero -> 'True :~: 'True
IsLongerOrSameLength out n :~: 'True
forall {k} (a :: k). a :~: a
Refl
  Succ PeanoNatural m
m -> case (forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
forall {k} (xs :: [k]). KList xs
assumeKnown @inp, forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
forall {k} (xs :: [k]). KList xs
assumeKnown @out) of
    (KCons Proxy x
_ (Proxy xs
_ :: Proxy inp'), KCons Proxy x
_ (Proxy xs
_ :: Proxy out')) ->
      'True :~: 'True
IsLongerOrSameLength xs m :~: 'True
(IsLongerOrSameLength xs m ~ 'True) =>
IsLongerOrSameLength xs m :~: 'True
forall {k} (a :: k). a :~: a
Refl ((IsLongerOrSameLength xs m ~ 'True) =>
 IsLongerOrSameLength xs m :~: 'True)
-> (IsLongerOrSameLength xs m :~: 'True)
-> IsLongerOrSameLength xs m :~: 'True
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (inp :: [k]) (out :: [k]) (s :: [k]) (n :: Peano).
(RequireLongerOrSameLength inp n, (LazyTake n inp ++ s) ~ out) =>
PeanoNatural n -> IsLongerOrSameLength out n :~: 'True
forall {k} (inp :: [k]) (out :: [k]) (s :: [k]) (n :: Peano).
(RequireLongerOrSameLength inp n, (LazyTake n inp ++ s) ~ out) =>
PeanoNatural n -> IsLongerOrSameLength out n :~: 'True
dipNExtensionLemma @inp' @out' @s PeanoNatural m
m

pairNExtensionThm
  :: forall s a n. (n >= ToPeano 2 ~ 'True, IsLongerOrSameLength a n ~ 'True)
  => PeanoNatural n
  -> Dict (ConstraintPairN n (a ++ s)
      , RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a)
      , Drop n (a ++ s) ~ (Drop n a ++ s)
      )
pairNExtensionThm :: forall (s :: [T]) (a :: [T]) (n :: Peano).
((n >= ToPeano 2) ~ 'True, IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n
-> Dict
     (ConstraintPairN n (a ++ s),
      RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a),
      Drop n (a ++ s) ~ (Drop n a ++ s))
pairNExtensionThm PeanoNatural n
n = Dict
  ((RequireLongerOrSameLength (a ++ s) n,
    (() :: Constraint, 'True ~ 'True)),
   RightComb (LazyTake n a) ~ RightComb (LazyTake n a),
   (Drop n a ++ s) ~ (Drop n a ++ s))
Dict
  ((RequireLongerOrSameLength (a ++ s) n,
    (() :: Constraint, 'True ~ 'True)),
   RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a),
   Drop n (a ++ s) ~ (Drop n a ++ s))
(IsLongerOrSameLength (a ++ s) n ~ 'True) =>
Dict
  ((RequireLongerOrSameLength (a ++ s) n,
    (() :: Constraint, 'True ~ 'True)),
   RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a),
   Drop n (a ++ s) ~ (Drop n a ++ s))
forall (a :: Constraint). a => Dict a
Dict
  ((IsLongerOrSameLength (a ++ s) n ~ 'True) =>
 Dict
   ((RequireLongerOrSameLength (a ++ s) n,
     (() :: Constraint, 'True ~ 'True)),
    RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a),
    Drop n (a ++ s) ~ (Drop n a ++ s)))
-> (IsLongerOrSameLength (a ++ s) n :~: 'True)
-> Dict
     ((RequireLongerOrSameLength (a ++ s) n,
       (() :: Constraint, 'True ~ 'True)),
      RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a),
      Drop n (a ++ s) ~ (Drop n a ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> IsLongerOrSameLength (a ++ s) n :~: 'True
isLongerOrSameLengthExtThm @a @s PeanoNatural n
n
  ((Drop n (a ++ s) ~ (Drop n a ++ s)) =>
 Dict
   ((RequireLongerOrSameLength (a ++ s) n,
     (() :: Constraint, 'True ~ 'True)),
    RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a),
    Drop n (a ++ s) ~ (Drop n a ++ s)))
-> (Drop n (a ++ s) :~: (Drop n a ++ s))
-> Dict
     ((RequireLongerOrSameLength (a ++ s) n,
       (() :: Constraint, 'True ~ 'True)),
      RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a),
      Drop n (a ++ s) ~ (Drop n a ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> Drop n (a ++ s) :~: (Drop n a ++ s)
dropExtensionThm @a @s PeanoNatural n
n
  ((LazyTake n (a ++ s) ~ LazyTake n a) =>
 Dict
   ((RequireLongerOrSameLength (a ++ s) n,
     (() :: Constraint, 'True ~ 'True)),
    RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a),
    Drop n (a ++ s) ~ (Drop n a ++ s)))
-> (LazyTake n (a ++ s) :~: LazyTake n a)
-> Dict
     ((RequireLongerOrSameLength (a ++ s) n,
       (() :: Constraint, 'True ~ 'True)),
      RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a),
      Drop n (a ++ s) ~ (Drop n a ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n -> LazyTake n (a ++ s) :~: LazyTake n a
takeExtensionThm @a @s PeanoNatural n
n

unpairNExtensionThm
  :: forall s a b n x r
    . ( a ~ x : r, CombedPairLeafCountIsAtLeast n x ~ 'True
      , n >= ToPeano 2 ~ 'True, UnpairN n x ++ r ~ b
      )
  => PeanoNatural n
  -> Dict (ConstraintUnpairN n x, UnpairN n x ++ r ++ s ~ b ++ s)
unpairNExtensionThm :: forall (s :: [T]) (a :: [T]) (b :: [T]) (n :: Peano) (x :: T)
       (r :: [T]).
(a ~ (x : r), CombedPairLeafCountIsAtLeast n x ~ 'True,
 (n >= ToPeano 2) ~ 'True, (UnpairN n x ++ r) ~ b) =>
PeanoNatural n
-> Dict
     (ConstraintUnpairN n x, (UnpairN n x ++ (r ++ s)) ~ (b ++ s))
unpairNExtensionThm PeanoNatural n
_ = Dict
  (((() :: Constraint, 'True ~ 'True),
    (() :: Constraint, 'True ~ 'True)),
   (UnpairN n x ++ (r ++ s)) ~ (b ++ s))
Dict
  (((() :: Constraint, 'True ~ 'True),
    (() :: Constraint, 'True ~ 'True)),
   (UnpairN n x ++ (r ++ s)) ~ (UnpairN n x ++ (r ++ s)))
((b ++ s) ~ (UnpairN n x ++ (r ++ s))) =>
Dict
  (((() :: Constraint, 'True ~ 'True),
    (() :: Constraint, 'True ~ 'True)),
   (UnpairN n x ++ (r ++ s)) ~ (b ++ s))
forall (a :: Constraint). a => Dict a
Dict (((b ++ s) ~ (UnpairN n x ++ (r ++ s))) =>
 Dict
   (((() :: Constraint, 'True ~ 'True),
     (() :: Constraint, 'True ~ 'True)),
    (UnpairN n x ++ (r ++ s)) ~ (b ++ s)))
-> ((b ++ s) :~: (UnpairN n x ++ (r ++ s)))
-> Dict
     (((() :: Constraint, 'True ~ 'True),
       (() :: Constraint, 'True ~ 'True)),
      (UnpairN n x ++ (r ++ s)) ~ (b ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (b :: [T]) (c :: [T]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
forall {k} (a :: [k]) (b :: [k]) (c :: [k]).
((a ++ b) ++ c) :~: (a ++ (b ++ c))
assocThm @(UnpairN n x) @r @s
  where Dict (a ~ (x : r))
_ = forall (a :: Constraint). a => Dict a
Dict @(a ~ x : r)