{-# LANGUAGE UndecidableInstances #-}

-- This Source Code Form is subject to the terms of the Mozilla Public
-- License, v. 2.0. If a copy of the MPL was not distributed with this
-- file, You can obtain one at https://mozilla.org/MPL/2.0/.

{- |
Copyright   :  (c) 2023 Yamada Ryo
License     :  MPL-2.0 (see the file LICENSE)
Maintainer  :  ymdfield@outlook.jp
Stability   :  experimental
Portability :  portable

A type class representing a general open union for higher-order effects, independent of the internal
implementation.
-}
module Data.Hefty.Union where

import Control.Effect.Class (Signature, type (~>))
import Data.Kind (Constraint)

{- |
A type class representing a general open union for higher-order effects, independent of the internal
implementation.
-}
class UnionH (u :: [Signature] -> Signature) where
    {-# MINIMAL injectH, projectH, absurdUnionH, (compH | (inject0H, weakenH), decompH | (|+:)) #-}

    type HasMembershipH u (h :: Signature) (hs :: [Signature]) :: Constraint

    injectH :: HasMembershipH u h hs => h f ~> u hs f
    projectH :: HasMembershipH u h hs => u hs f a -> Maybe (h f a)

    absurdUnionH :: u '[] f a -> x

    compH :: Either (h f a) (u hs f a) -> u (h ': hs) f a
    compH = \case
        Left h f a
x -> forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H h f a
x
        Right u hs f a
x -> forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h : hs) f
weakenH u hs f a
x
    {-# INLINE compH #-}

    decompH :: u (h ': hs) f a -> Either (h f a) (u hs f a)
    decompH = forall a b. a -> Either a b
Left forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall a b. b -> Either a b
Right
    {-# INLINE decompH #-}

    infixr 5 |+:
    (|+:) :: (h f a -> r) -> (u hs f a -> r) -> u (h ': hs) f a -> r
    (h f a -> r
f |+: u hs f a -> r
g) u (h : hs) f a
u = case forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (hs :: [(* -> *) -> * -> *])
       (f :: * -> *) a.
UnionH u =>
u (h : hs) f a -> Either (h f a) (u hs f a)
decompH u (h : hs) f a
u of
        Left h f a
x -> h f a -> r
f h f a
x
        Right u hs f a
x -> u hs f a -> r
g u hs f a
x
    {-# INLINE (|+:) #-}

    inject0H :: h f ~> u (h ': hs) f
    inject0H = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
Either (h f a) (u hs f a) -> u (h : hs) f a
compH forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left
    {-# INLINE inject0H #-}

    injectUnderH :: h2 f ~> u (h1 ': h2 ': hs) f
    injectUnderH = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h : hs) f
weakenH forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H
    {-# INLINE injectUnderH #-}

    injectUnder2H :: h3 f ~> u (h1 ': h2 ': h3 ': hs) f
    injectUnder2H = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : hs) f
weaken2H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H
    {-# INLINE injectUnder2H #-}

    injectUnder3H :: h4 f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f
    injectUnder3H = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : hs) f
weaken3H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H
    {-# INLINE injectUnder3H #-}

    weakenH :: u hs f ~> u (h ': hs) f
    weakenH = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
Either (h f a) (u hs f a) -> u (h : hs) f a
compH forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right
    {-# INLINE weakenH #-}

    weaken2H :: u hs f ~> u (h1 ': h2 ': hs) f
    weaken2H = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h : hs) f
weakenH forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h : hs) f
weakenH
    {-# INLINE weaken2H #-}

    weaken3H :: u hs f ~> u (h1 ': h2 ': h3 ': hs) f
    weaken3H = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : hs) f
weaken2H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h : hs) f
weakenH
    {-# INLINE weaken3H #-}

    weaken4H :: u hs f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f
    weaken4H = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : hs) f
weaken3H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h : hs) f
weakenH
    {-# INLINE weaken4H #-}

    weakenUnderH :: u (h1 ': hs) f ~> u (h1 ': h2 ': hs) f
    weakenUnderH = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : hs) f
weaken2H

    weakenUnder2H :: u (h1 ': h2 ': hs) f ~> u (h1 ': h2 ': h3 ': hs) f
    weakenUnder2H = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : hs) f
weaken3H

    weakenUnder3H :: u (h1 ': h2 ': h3 ': hs) f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f
    weakenUnder3H = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h3 f ~> u (h1 : h2 : h3 : hs) f
injectUnder2H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *) (h4 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : h4 : hs) f
weaken4H

    weaken2UnderH :: u (h1 ': hs) f ~> u (h1 ': h2 ': h3 ': hs) f
    weaken2UnderH = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : hs) f
weaken3H

    weaken2Under2H :: u (h1 ': h2 ': hs) f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f
    weaken2Under2H = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *) (h4 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : h4 : hs) f
weaken4H

    weaken3UnderH :: u (h1 ': hs) f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f
    weaken3UnderH = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *) (h4 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : h4 : hs) f
weaken4H

    flipUnionH :: u (h1 ': h2 ': hs) f ~> u (h2 ': h1 ': hs) f
    flipUnionH = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : hs) f
weaken2H

    flipUnion3H :: u (h1 ': h2 ': h3 ': hs) f ~> u (h3 ': h2 ': h1 ': hs) f
    flipUnion3H = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h3 f ~> u (h1 : h2 : h3 : hs) f
injectUnder2H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : hs) f
weaken3H

    flipUnionUnderH :: u (h1 ': h2 ': h3 ': hs) f ~> u (h1 ': h3 ': h2 ': hs) f
    flipUnionUnderH = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h3 f ~> u (h1 : h2 : h3 : hs) f
injectUnder2H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : hs) f
weaken3H

    rot3H :: u (h1 ': h2 ': h3 ': hs) f ~> u (h2 ': h3 ': h1 ': hs) f
    rot3H = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h3 f ~> u (h1 : h2 : h3 : hs) f
injectUnder2H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : hs) f
weaken3H

    rot3H' :: u (h1 ': h2 ': h3 ': hs) f ~> u (h3 ': h1 ': h2 ': hs) f
    rot3H' = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h3 f ~> u (h1 : h2 : h3 : hs) f
injectUnder2H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : hs) f
weaken3H

    bundleUnion2H :: UnionH u' => u (h1 ': h2 ': hs) f ~> u (u' '[h1, h2] ': hs) f
    bundleUnion2H = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h : hs) f
weakenH

    bundleUnion3H :: UnionH u' => u (h1 ': h2 ': h3 ': hs) f ~> u (u' '[h1, h2, h3] ': hs) f
    bundleUnion3H =
        (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H)
            forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH)
            forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h3 f ~> u (h1 : h2 : h3 : hs) f
injectUnder2H)
            forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h : hs) f
weakenH

    bundleUnion4H ::
        UnionH u' =>
        u (h1 ': h2 ': h3 ': h4 ': hs) f ~> u (u' '[h1, h2, h3, h4] ': hs) f
    bundleUnion4H =
        (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H)
            forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH)
            forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h3 f ~> u (h1 : h2 : h3 : hs) f
injectUnder2H)
            forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h4 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (h3 :: (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h4 f ~> u (h1 : h2 : h3 : h4 : hs) f
injectUnder3H)
            forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h : hs) f
weakenH

    unbundleUnion2H :: UnionH u' => u (u' '[h1, h2] ': hs) f ~> u (h1 ': h2 ': hs) f
    unbundleUnion2H = (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (f :: * -> *) a x.
UnionH u =>
u '[] f a -> x
absurdUnionH) forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : hs) f
weaken2H

    unbundleUnion3H :: UnionH u' => u (u' '[h1, h2, h3] ': hs) f ~> u (h1 ': h2 ': h3 ': hs) f
    unbundleUnion3H = (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h3 f ~> u (h1 : h2 : h3 : hs) f
injectUnder2H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (f :: * -> *) a x.
UnionH u =>
u '[] f a -> x
absurdUnionH) forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : hs) f
weaken3H

    unbundleUnion4H ::
        UnionH u' =>
        u (u' '[h1, h2, h3, h4] ': hs) f
            ~> u (h1 ': h2 ': h3 ': h4 ': hs) f
    unbundleUnion4H =
        (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h3 f ~> u (h1 : h2 : h3 : hs) f
injectUnder2H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h4 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (h3 :: (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h4 f ~> u (h1 : h2 : h3 : h4 : hs) f
injectUnder3H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (f :: * -> *) a x.
UnionH u =>
u '[] f a -> x
absurdUnionH)
            forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h :: (* -> *) -> * -> *) (f :: * -> *) a r
       (hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (hs :: [(* -> *) -> * -> *]) (f :: * -> *)
       (h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *) (h4 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : h4 : hs) f
weaken4H

type family IsMemberH (h :: Signature) hs where
    IsMemberH h (h ': hs) = 'True
    IsMemberH h (_ ': hs) = IsMemberH h hs
    IsMemberH _ '[] = 'False

type MemberH u h hs = (HasMembershipH u h hs, IsMemberH h hs ~ 'True)