diff --git a/deptycheck.ipkg b/deptycheck.ipkg
index b015e8cce..4740411be 100644
--- a/deptycheck.ipkg
+++ b/deptycheck.ipkg
@@ -39,5 +39,6 @@ depends = ansi
         , if-unsolved-implicit
         , mtl-tuple-impls
         , positive-nat
+        , proof-utils
         , random-pure
         , typelevel-emptiness-collections
diff --git a/pack.toml b/pack.toml
index 5988053e0..a0861e7bf 100644
--- a/pack.toml
+++ b/pack.toml
@@ -20,6 +20,16 @@ type = "local"
 path = "docs"
 ipkg = "docs.ipkg"
 
+###################
+### Proof utils ###
+###################
+
+[custom.all.proof-utils]
+type   = "git"
+url    = "https://github.com/spcfox/idris2-proof-utils.git"
+commit = "1e7e63b147fcdab9a2e9247646e7494485f6ca15"
+ipkg   = "proof-utils.ipkg"
+
 ################
 ### Examples ###
 ################
diff --git a/src/Test/DepTyCheck/Gen.idr b/src/Test/DepTyCheck/Gen.idr
index 47020264e..26c0eebe3 100644
--- a/src/Test/DepTyCheck/Gen.idr
+++ b/src/Test/DepTyCheck/Gen.idr
@@ -7,22 +7,32 @@ import public Control.Monad.Random.Interface
 
 import Data.Bool
 import public Data.CheckedEmpty.List.Lazy
+import Data.CheckedEmpty.List.Lazy.Properties
+import Control.Foldable.Quantifiers
 import Data.Fuel
 import public Data.Nat1
 import Data.List
+import Data.List.Elem
+import Data.List.Properties
+import Data.List.Quantifiers.Properties
 import Data.List.Lazy
 import Data.List.Lazy.Extra
+import Data.So.Utils
 import Data.Vect
 
 import Decidable.Equality
 
 import public Language.Implicits.IfUnsolved
 
-import Syntax.WithProof
+import Syntax.WithProof.Extra
 
 import public Test.DepTyCheck.Gen.Emptiness
 import public Test.DepTyCheck.Gen.Labels
 
+%hide Control.Foldable.Elem.Elem
+%hide Control.Foldable.Elem.elemMap
+%hide Control.Foldable.Quantifiers.All
+
 %default total
 
 -------------------------
@@ -40,6 +50,9 @@ wrapLazy f = delay . f . force
 wrapMaybeTaggedLazy : (a -> Maybe b) -> (tag, Lazy a) -> Maybe (tag, Lazy b)
 wrapMaybeTaggedLazy f = traverse $ map delay . f . force
 
+0 unpackTaggedLazy : Foldable f => f (tag, Lazy a) -> List a
+unpackTaggedLazy = map (force . snd) . toList
+
 -------------------------------
 --- Definition of the `Gen` ---
 -------------------------------
@@ -49,9 +62,15 @@ record RawGen a where
   unRawGen : forall m. MonadRandom m => CanManageLabels m => m a
 
 export
-record GenAlternatives (0 mustBeNotEmpty : Bool) (0 em : Emptiness) (a : Type)
+data Gen : Emptiness -> Type -> Type
+
+0 IsNonEmpty : Gen em a -> Type
 
 export
+record GenAlternatives (0 mustBeNotEmpty : Bool) (0 em : Emptiness) (a : Type)
+
+0 All : (Gen em a -> Type) -> GenAlternatives ne em a -> Type
+
 data Gen : Emptiness -> Type -> Type where
 
   Empty : Gen MaybeEmpty a
@@ -60,20 +79,48 @@ data Gen : Emptiness -> Type -> Type where
 
   Raw   : RawGen a -> Gen em a
 
-  OneOf : (0 _ : alem `NoWeaker` em) =>
-          (0 _ : NotImmediatelyEmpty alem) =>
-          GenAlternatives True alem a -> Gen em a
+  OneOf : (gs : GenAlternatives True alem a) ->
+          (0 _ : All IsNonEmpty gs) =>
+          (0 _ : alem `NoWeaker` em) =>
+          Gen em a
 
   Bind  : {biem : _} ->
-          (0 _ : BindToOuter biem em) =>
+          (0 _ : biem `NoWeaker` em) =>
           RawGen c -> (c -> Gen biem a) -> Gen em a
 
-  Labelled : Label -> Gen em a -> Gen em a
+  Labelled : Label -> (g : Gen em a) -> (0 _ : IsNonEmpty g) => Gen em a
+
+isEmpty : Gen em a -> Bool
+isEmpty Empty = True
+isEmpty _     = False
+
+%inline
+isNonEmpty : Gen em a -> Bool
+isNonEmpty = not . isEmpty
+
+IsNonEmpty = So . isNonEmpty
+
+IsEmpty : Gen em a -> Type
+IsEmpty = So . isEmpty
 
 record GenAlternatives (0 mustBeNotEmpty : Bool) (0 em : Emptiness) (a : Type) where
   constructor MkGenAlts
   unGenAlts : LazyLst mustBeNotEmpty (Nat1, Lazy (Gen em a))
 
+0 listOfAlts : GenAlternatives ne em a -> List $ Gen em a
+listOfAlts $ MkGenAlts gs = unpackTaggedLazy gs
+
+All p = All p . listOfAlts
+
+0 Elem : Gen em a -> GenAlternatives ne em a -> Type
+Elem g = Elem g . listOfAlts
+
+0 DecIsEmpty : (g : Gen em a) -> Type
+DecIsEmpty = Subset Bool . BoolWithProof . isEmpty
+
+decIsEmpty : (g : Gen em a) -> DecIsEmpty g
+decIsEmpty g = boolWithProof $ isEmpty g
+
 (.totalWeight) : GenAlternatives True em a -> Nat1
 (.totalWeight) = foldl1 (+) . map fst . unGenAlts
 
@@ -89,6 +136,14 @@ public export %inline
 Gen0 : Type -> Type
 Gen0 = Gen MaybeEmpty
 
+%hint
+0 isNonEmptyGen1 : {g : Gen1 a} -> IsNonEmpty g
+isNonEmptyGen1 {g=Pure _}       = Oh
+isNonEmptyGen1 {g=Raw _}        = Oh
+isNonEmptyGen1 {g=OneOf _}      = Oh
+isNonEmptyGen1 {g=Bind _ _}     = Oh
+isNonEmptyGen1 {g=Labelled _ _} = Oh
+
 -----------------------------
 --- Very basic generators ---
 -----------------------------
@@ -111,30 +166,64 @@ empty = Empty
 
 export
 label : Label -> Gen em a -> Gen em a
-label _ Empty = Empty
-label l g     = Labelled l g
+label l g with (decIsEmpty g)
+  label _ Empty | Element True  _ = Empty
+  label l g     | Element False _ = Labelled l g
 
 ------------------------------------------------
 --- Technical stuff for mapping alternatives ---
 ------------------------------------------------
 
 mapTaggedLazy : Functor f => (a -> b) -> f (tag, Lazy a) -> f (tag, Lazy b)
-mapTaggedLazy = map . mapSnd . wrapLazy
+mapTaggedLazy f = map $ \x => (fst x, wrapLazy f $ snd x)
 
 mapOneOf : GenAlternatives ne iem a -> (Gen iem a -> Gen em b) -> GenAlternatives ne em b
-mapOneOf oo f = MkGenAlts $ mapTaggedLazy f oo.unGenAlts
-
-mapMaybeTaggedLazy : (a -> Maybe b) -> LazyLst ne (Nat1, Lazy a) -> LazyLst0 (Nat1, Lazy b)
-mapMaybeTaggedLazy = mapMaybe . wrapMaybeTaggedLazy
-
-traverseMaybe : (a -> Maybe b) -> LazyLst ne a -> Maybe $ LazyLst ne b
-traverseMaybe f []      = Just []
-traverseMaybe f (x::xs) = case f x of
-  Nothing => Nothing
-  Just y  => (y ::) <$> traverseMaybe f xs
-
-trMOneOf : GenAlternatives ne iem a -> (Gen iem a -> Maybe $ Gen em b) -> Maybe $ GenAlternatives ne em b
-trMOneOf oo = map MkGenAlts . flip traverseMaybe oo.unGenAlts . wrapMaybeTaggedLazy
+mapOneOf $ MkGenAlts gs = MkGenAlts . flip mapTaggedLazy gs
+
+0 allMapTaggedLazy : (0 _ : Functor t) => Foldable t => LawfulFoldableFunctor t =>
+                     {0 f : a -> b} -> {xs : t (tag, Lazy a)} ->
+                     ({x : a} -> (0 _ : Elem x $ unpackTaggedLazy xs) -> p $ f x) ->
+                     All p $ unpackTaggedLazy $ mapTaggedLazy f xs
+allMapTaggedLazy h = allMap {t=List} $ allMapForall {t} $ \e => h $ elemMap _ e
+
+0 allMapOneOf : {0 f : Gen iem a -> Gen em b} ->
+                {gs : GenAlternatives ne iem a} ->
+                ({x : Gen iem a} -> (0 _ : Elem x gs) -> p $ f x) ->
+                All p $ mapOneOf gs f
+allMapOneOf {gs=MkGenAlts _} = allMapTaggedLazy {t=LazyLst ne}
+
+mapElem : (xs : LazyLst ne a) -> ((x : a) -> (0 _ : Elem x $ toList xs) -> b) -> LazyLst ne b
+mapElem []        _ = []
+mapElem (x :: xs) f = f x Here :: mapElem xs (\y, e => f y $ There e)
+
+mapTaggedLazyElem : (xs : LazyLst ne (tag, Lazy a)) ->
+                    ((x : a) -> (0 _ : Elem x $ unpackTaggedLazy xs) -> b) ->
+                    LazyLst ne (tag, Lazy b)
+mapTaggedLazyElem xs f = mapElem xs $ \x, e => (fst x, delay $ f (snd x) $ elemMap _ e)
+
+mapOneOfElem : (gs : GenAlternatives ne iem a) ->
+               ((g : Gen iem a) -> (0 _ : Elem g gs) -> Gen em b) ->
+               GenAlternatives ne em b
+mapOneOfElem $ MkGenAlts gs = MkGenAlts . mapTaggedLazyElem gs
+
+0 allMapElem : {xs : LazyLst ne a} ->
+               {0 f : (x : a) -> (0 _ : Elem x $ toList xs) -> b} ->
+               ({x : a} -> (0 e : Elem x $ toList xs) -> p $ f x e) ->
+               All p $ toList $ mapElem xs f
+allMapElem {xs=[]}      _ = []
+allMapElem {xs=x :: xs} h = h Here :: allMapElem (\e => h $ There e)
+
+0 allMapTaggedLazyElem : {xs : LazyLst ne (tag, Lazy a)} ->
+                         {0 f : (x : a) -> (0 _ : Elem x $ unpackTaggedLazy xs) -> b} ->
+                         ({x : a} -> (0 e : Elem x $ unpackTaggedLazy xs) -> p $ f x e) ->
+                         All p $ unpackTaggedLazy $ mapTaggedLazyElem xs f
+allMapTaggedLazyElem h = allMap {t=List} $ allMapElem $ \e => h $ elemMap _ e
+
+0 allMapOneOfElem : {gs : GenAlternatives ne iem a} ->
+                    {0 f : (g : Gen iem a) -> (0 _ : Elem g gs) -> Gen em b} ->
+                    ({g : Gen iem a} -> (0 e : Elem g gs) -> p $ f g e) ->
+                    All p $ mapOneOfElem gs f
+allMapOneOfElem {gs=MkGenAlts _} = allMapTaggedLazyElem
 
 -----------------------------
 --- Emptiness tweakenings ---
@@ -142,43 +231,55 @@ trMOneOf oo = map MkGenAlts . flip traverseMaybe oo.unGenAlts . wrapMaybeTaggedL
 
 export
 relax : (0 _ : iem `NoWeaker` em) => Gen iem a -> Gen em a
-relax @{nw} Empty      = rewrite maybeEmptyIsMinimal nw in Empty
-relax $ Pure x         = Pure x
-relax $ Raw x          = Raw x
-relax $ OneOf @{wo} x  = OneOf @{transitive' wo %search} x
-relax $ Bind @{bo} x f = Bind @{bindToOuterRelax bo %search} x f
-relax $ Labelled l x   = label l $ relax x
-
-export
-strengthen : {em : _} -> Gen iem a -> Maybe $ Gen em a
+0 relaxNonEmpty : {g : Gen iem a} -> IsNonEmpty g => IsNonEmpty $ relax @{nw} g
 
-strengthen {em=MaybeEmpty} Empty = Just Empty
-strengthen {em=_}          Empty = Nothing
+relax @{nw} Empty           = rewrite maybeEmptyIsMinimal nw in Empty
+relax $ Pure x              = Pure x
+relax $ Raw x               = Raw x
+relax $ OneOf @{ne} @{nw} x = OneOf @{ne} @{transitive' nw %search} x
+relax $ Bind @{nw} x f      = Bind @{transitive' nw %search} x f
+relax $ Labelled l x        = Labelled @{relaxNonEmpty} l $ relax x
 
-strengthen $ Pure x = Just $ Pure x
-strengthen $ Raw x  = Just $ Raw x
-
-strengthen $ OneOf @{_} @{au} x with (decCanBeEmpty em)
-  _ | Yes _ = Just $ OneOf @{relaxAnyCanBeEmpty au} @{au} x
-  _ | No  _ = map OneOf $ trMOneOf x $ assert_total $ strengthen {em=NonEmpty}
-
-strengthen $ Bind {biem} x f with (decCanBeEmpty em)
-  _ | Yes _ = Just $ Bind x f
-  _ | No  _ = case biem of
-    NonEmpty => Just $ Bind x f
-    _        => Nothing
-
-strengthen $ Labelled l x = label l <$> strengthen x
+relaxNonEmpty {g=Pure _}       = Oh
+relaxNonEmpty {g=Raw _}        = Oh
+relaxNonEmpty {g=OneOf _}      = Oh
+relaxNonEmpty {g=Bind _ _}     = Oh
+relaxNonEmpty {g=Labelled _ _} = Oh
 
 --------------------
 --- More utility ---
 --------------------
 
-mkOneOf : (0 _ : alem `NoWeaker` em) =>
-          (0 _ : NotImmediatelyEmpty alem) =>
-          (gens : LazyLst1 (Nat1, Lazy (Gen alem a))) ->
+namespace OneOf
+
+  public export
+  data AltsNonEmpty : Bool -> Emptiness -> Type where
+    NT : AltsNonEmpty True   NonEmpty
+    Sx : AltsNonEmpty altsNe MaybeEmpty
+
+  export %defaulthint
+  altsNonEmptyTrue : {em : _} -> AltsNonEmpty True em
+  altsNonEmptyTrue {em=NonEmpty}   = NT
+  altsNonEmptyTrue {em=MaybeEmpty} = Sx
+
+mkOneOfMaybeEmpty : (xs : LazyLst altsNe (Nat1, Lazy (Gen alem a))) ->
+                    (0 _ : All IsNonEmpty $ unpackTaggedLazy xs) =>
+                    Gen0 a
+mkOneOfMaybeEmpty []        = Empty
+mkOneOfMaybeEmpty (x :: xs) = OneOf $ MkGenAlts $ x :: xs
+
+mkOneOf : {em : _} ->
+          (0 _ : alem `NoWeaker` em) =>
+          (0 _ : AltsNonEmpty altsNe em) =>
+          LazyLst altsNe (Nat1, Lazy (Gen alem a)) ->
           Gen em a
-mkOneOf gens = OneOf $ MkGenAlts gens
+mkOneOf {em=NonEmpty} @{nw} @{NT} xs with 0 (nonEmptyIsMaximal nw)
+  _ | Refl = OneOf @{allTrue isNonEmptyGen1} $ MkGenAlts xs
+-- TODO: filter has problem with laziness
+-- mkOneOf {em=MaybeEmpty} xs = mkOneOfMaybeEmpty @{allMap {t=List} filterElem} $ filter (isNonEmpty . force . snd) xs
+-- Not using mapSnd, because it's less reducible.
+mkOneOf {em=MaybeEmpty} xs = mkOneOfMaybeEmpty @{allMap {t=List} $ allMap {t=LazyLst False} $ filterElem} $
+  map (\x => (fst x, delay $ snd x)) $ filter (isNonEmpty . snd) $ map (\x => (fst x, force $ snd x)) xs
 
 --------------------------
 --- Running generators ---
@@ -190,9 +291,9 @@ export
 unGen1 : MonadRandom m => CanManageLabels m => Gen1 a -> m a
 unGen1 $ Pure x         = pure x
 unGen1 $ Raw sf         = sf.unRawGen
-unGen1 $ OneOf @{nw} oo with 0 (nonEmptyIsMaximal nw)
+unGen1 $ OneOf @{_} @{nw} oo with 0 (nonEmptyIsMaximal nw)
   _ | Refl = assert_total unGen1 . force . pickWeighted oo.unGenAlts . finToNat =<< randomFin oo.totalWeight
-unGen1 $ Bind @{bo} x f with 0 (extractNE bo)
+unGen1 $ Bind @{nw} x f with 0 (nonEmptyIsMaximal nw)
   _ | Refl = x.unRawGen >>= unGen1 . f
 unGen1 $ Labelled l x   = manageLabel l $ unGen1 x
 
@@ -243,7 +344,7 @@ unGenTryN n = mapMaybe id .: take (limit n) .: unGenTryAll
 ||| Tries once to pick a random value from a generator
 export
 pick : CanInitSeed g m => Functor m => Gen em a -> m $ Maybe a
-pick gen = initSeed <&> \s => evalRandom s $ unGen' gen
+pick gen = initSeed <&> flip evalRandom (unGen' gen)
 
 ||| Tries to pick a random value from a generator, returning the number of unsuccessful attempts, if generated successfully
 export
@@ -270,69 +371,102 @@ Applicative RawGen where
   MkRawGen x <*> MkRawGen y = MkRawGen $ x <*> y
 
 --- `Gen` ---
-
 export
-Functor (Gen em) where
-  map f $ Empty        = Empty
-  map f $ Pure x       = Pure $ f x
-  map f $ Raw sf       = Raw $ f <$> sf
-  map f $ OneOf oo     = OneOf $ mapOneOf oo $ assert_total $ map f
-  map f $ Bind x g     = Bind x $ map f . g
-  map f $ Labelled l x = label l $ map f x
-
-namespace GenAlternatives
+Functor (Gen em)
+0 mapNonEmpty : {g : Gen iem a} -> IsNonEmpty g => IsNonEmpty $ f <$> g
 
-  export %inline
-  strengthen : GenAlternatives ne em a -> Maybe $ GenAlternatives True em a
-  strengthen = map MkGenAlts . strengthen . unGenAlts
+Functor (Gen em) where
+  map f $ Empty          = Empty
+  map f $ Pure x         = Pure $ f x
+  map f $ Raw sf         = Raw $ f <$> sf
+  map f $ OneOf @{ne} oo = OneOf @{allMapOneOf $ \e => mapNonEmpty @{indexAll e ne}} $ mapOneOf oo $ assert_total $ map f
+  map f $ Bind x g       = Bind x $ map f . g
+  map f $ Labelled l x   = Labelled @{mapNonEmpty} l $ map f x
 
-  export %inline
-  mapMaybe : (Gen iem a -> Maybe (Gen em b)) -> GenAlternatives ne iem a -> GenAlternatives False em b
-  mapMaybe f = MkGenAlts . mapMaybeTaggedLazy f . unGenAlts
+mapNonEmpty {g=Pure _}       = Oh
+mapNonEmpty {g=Raw _}        = Oh
+mapNonEmpty {g=OneOf _}      = Oh
+mapNonEmpty {g=Bind _ _}     = Oh
+mapNonEmpty {g=Labelled _ _} = Oh
 
 export
-{em : _} -> Applicative (Gen em) where
+Applicative (Gen em)
+0 apNonEmpty : {g : Gen em $ a -> b} -> {h : Gen em a} -> IsNonEmpty g => IsNonEmpty h => IsNonEmpty $ g <*> h
+
+Applicative (Gen em) where
 
   pure = Pure
 
-  Empty <*> _ = Empty
-  _ <*> Empty = Empty
+  g <*> h with (decIsEmpty g) | (decIsEmpty h)
+    Empty <*> _ | _ | _ = Empty
+    _ <*> Empty | _ | _ = Empty
+
+    Pure f <*> g | _ | _ = f <$> g
+    g <*> Pure x | _ | _ = g <&> \f => f x
+
+    Raw sfl <*> Raw sfr | _ | _ = Raw $ sfl <*> sfr
+
+    Labelled l x <*> y | _ | Element False _ = Labelled @{apNonEmpty} l $ x <*> y
+    x <*> Labelled l y | Element False _ | _ = Labelled @{apNonEmpty} l $ x <*> y
+
+    OneOf @{ne} oo <*> g | _ | Element False _ =
+      OneOf @{allMapOneOf $ \e => apNonEmpty @{relaxNonEmpty @{indexAll e ne}}} $
+        mapOneOf oo $ \x => assert_total $ relax x <*> g
+    g <*> OneOf @{ne} oo | Element False _ | _ =
+      OneOf @{allMapOneOf $ \e => apNonEmpty @{%search} @{relaxNonEmpty @{indexAll e ne}}} $
+        mapOneOf oo $ \x => assert_total $ g <*> relax x
+
+    Bind x f <*> Raw y | _ | _ = Bind x $ \c => f c <*> Raw y
+    Raw y <*> Bind x f | _ | _ = Bind x $ \c => assert_total $ Raw y <*> f c
+
+    Bind {biem=bl} x f <*> Bind {biem=br} y g | _ | _ = case order {rel=NoWeaker} bl br of
+      Left  _ => Bind [| (x, y) |] $ \(l, r) => assert_total $ relax (f l) <*> g r
+      Right _ => Bind [| (x, y) |] $ \(l, r) => f l <*> relax (g r)
+
+apNonEmpty with (decIsEmpty g) | (decIsEmpty h)
+  apNonEmpty {g=Pure _}       {h=Pure _}       | _               | _               = Oh
+  apNonEmpty {g=Pure _}       {h=Raw _}        | _               | _               = Oh
+  apNonEmpty {g=Pure _}       {h=OneOf _}      | _               | _               = Oh
+  apNonEmpty {g=Pure _}       {h=Bind _ _}     | _               | _               = Oh
+  apNonEmpty {g=Pure _}       {h=Labelled _ _} | _               | _               = Oh
+
+  apNonEmpty {g=Raw _}        {h=Pure _}       | _               | _               = Oh
+  apNonEmpty {g=OneOf _}      {h=Pure _}       | _               | _               = Oh
+  apNonEmpty {g=Bind _ _}     {h=Pure _}       | _               | _               = Oh
+  apNonEmpty {g=Labelled _ _} {h=Pure _}       | _               | _               = Oh
+
+  apNonEmpty {g=Raw _}        {h=Raw _}        | _               | _               = Oh
 
-  Pure f <*> g = f <$> g
-  g <*> Pure x = g <&> \f => f x
+  apNonEmpty {g=Labelled _ _} {h=Raw _}        | _               | Element False _ = Oh
+  apNonEmpty {g=Labelled _ _} {h=OneOf _}      | _               | Element False _ = Oh
+  apNonEmpty {g=Labelled _ _} {h=Bind _ _}     | _               | Element False _ = Oh
+  apNonEmpty {g=Labelled _ _} {h=Labelled _ _} | _               | Element False _ = Oh
 
-  Raw sfl <*> Raw sfr = Raw $ sfl <*> sfr
+  apNonEmpty {g=Raw _}        {h=Labelled _ _} | Element False _ | Element False _ = Oh
+  apNonEmpty {g=OneOf _}      {h=Labelled _ _} | Element False _ | Element False _ = Oh
+  apNonEmpty {g=Bind _ _}     {h=Labelled _ _} | Element False _ | Element False _ = Oh
 
-  Labelled l x <*> y = label l $ x <*> y
-  x <*> Labelled l y = label l $ x <*> y
+  apNonEmpty {g=OneOf _}      {h=Raw _}        | _       False   | Element False _ = Oh
+  apNonEmpty {g=OneOf _}      {h=OneOf _}      | _       False   | Element False _ = Oh
+  apNonEmpty {g=OneOf _}      {h=Bind _ _}     | _       False   | Element False _ = Oh
 
-  OneOf oo <*> g = case canBeNotImmediatelyEmpty em of
-    Right _   => OneOf $ mapOneOf oo $ \x => assert_total $ relax x <*> g
-    Left Refl => maybe Empty (\g => OneOf $ mapOneOf oo $ \x => assert_total $ relax x <*> g) $ strengthen {em=MaybeEmptyDeep} g
-  g <*> OneOf oo = case canBeNotImmediatelyEmpty em of
-    Right _   => OneOf $ mapOneOf oo $ \x => assert_total $ g <*> relax x
-    Left Refl => maybe Empty (\g => OneOf $ mapOneOf oo $ \x => assert_total $ g <*> relax x) $ strengthen {em=MaybeEmptyDeep} g
+  apNonEmpty {g=Bind _ _}     {h=OneOf _}      | Element False _ | Element False _ = Oh
+  apNonEmpty {g=Raw _}        {h=OneOf _}      | Element False _ | Element False _ = Oh
 
-  Bind x f <*> Raw y = Bind x $ \c => f c <*> Raw y
-  Raw y <*> Bind x f = Bind x $ \c => assert_total $ Raw y <*> f c
+  apNonEmpty {g=Raw _}        {h=Bind _ _}     | _               | Element False _ = Oh
+  apNonEmpty {g=Bind _ _}     {h=Raw _}        | _               | Element False _ = Oh
 
-  Bind {biem=bl} x f <*> Bind {biem=br} y g = case order {rel=NoWeaker} bl br of
-    Left  _ => Bind [| (x, y) |] $ \(l, r) => assert_total $ relax (f l) <*> g r
-    Right _ => Bind [| (x, y) |] $ \(l, r) => f l <*> relax (g r)
+  apNonEmpty {g=Bind {biem=bl} _ _} {h=Bind {biem=br} _ _} | _   | Element False _ with (order {rel=NoWeaker} bl br)
+    _ | Left  _ = Oh
+    _ | Right _ = Oh
 
 export
 {em : _} -> Monad (Gen em) where
-  Empty    >>= _  = Empty
-  Pure x   >>= nf = nf x
-  Raw g    >>= nf = Bind g nf
-  (OneOf @{ao} oo >>= nf) {em=NonEmpty} with 0 (nonEmptyIsMaximal ao)
-    _ | Refl = OneOf $ mapOneOf oo $ assert_total $ (>>= nf)
-  (OneOf @{ao} oo >>= nf) {em=MaybeEmptyDeep} = OneOf $ mapOneOf oo $ assert_total (>>= nf) . relax @{ao}
-  (OneOf {alem} oo >>= nf) {em=MaybeEmpty} = maybe Empty (OneOf {alem=MaybeEmptyDeep}) $
-    strengthen $ flip mapMaybe oo $ strengthen . assert_total (>>= nf) . relax
-  Bind {biem} x f >>= nf with (order {rel=NoWeaker} biem em)
-    _ | Left _  = Bind x $ \x => assert_total $ relax (f x) >>= nf
-    _ | Right _ = Bind x $ \x => f x >>= relax . nf
+  Empty        >>= _  = Empty
+  Pure x       >>= nf = nf x
+  Raw g        >>= nf = Bind g nf
+  OneOf oo     >>= nf = mkOneOf $ flip mapTaggedLazy oo.unGenAlts $ assert_total (>>= nf) . relax
+  Bind x f     >>= nf = Bind x $ assert_total (>>= nf) . relax . f
   Labelled l x >>= nf = label l $ x >>= nf
 
 -----------------------------------------
@@ -396,48 +530,38 @@ namespace GenAlternatives
   relax : GenAlternatives True em a -> GenAlternatives ne em a
   relax = MkGenAlts . relaxT . unGenAlts
 
+  export %inline
+  strengthen : GenAlternatives ne em a -> Maybe $ GenAlternatives True em a
+  strengthen = map MkGenAlts . strengthen . unGenAlts
+
   export
   Functor (GenAlternatives ne em) where
     map = processAlternatives . map
 
   export
-  {em : _} -> Applicative (GenAlternatives ne em) where
+  Applicative (GenAlternatives ne em) where
     pure x = [ pure x ]
     xs <*> ys = flip processAlternatives' xs $ flip processAlternatives ys . (<*>)
 
   export
-  {em : _} -> Alternative (GenAlternatives False em) where
+  Alternative (GenAlternatives False em) where
     empty = []
     xs <|> ys = MkGenAlts $ xs.unGenAlts <|> ys.unGenAlts
 
   -- implementation for `Monad` is below --
 
 export
-{em : _} -> Cast (LazyLst ne a) (GenAlternatives ne em a) where
+Cast (LazyLst ne a) (GenAlternatives ne em a) where
   cast = MkGenAlts . map (\x => (1, pure x))
 
 public export %inline
-altsFromList : {em : _} -> LazyLst ne a -> GenAlternatives ne em a
+altsFromList : LazyLst ne a -> GenAlternatives ne em a
 altsFromList = cast
 
 ----------------------------------
 --- Creation of new generators ---
 ----------------------------------
 
-namespace OneOf
-
-  public export
-  data AltsNonEmpty : Bool -> Emptiness -> Type where
-    NT : AltsNonEmpty True   NonEmpty
-    DT : AltsNonEmpty True   MaybeEmptyDeep
-    Sx : AltsNonEmpty altsNe MaybeEmpty
-
-  export %defaulthint
-  altsNonEmptyTrue : {em : _} -> AltsNonEmpty True em
-  altsNonEmptyTrue {em=NonEmpty}       = NT
-  altsNonEmptyTrue {em=MaybeEmptyDeep} = DT
-  altsNonEmptyTrue {em=MaybeEmpty}     = Sx
-
 ||| Choose one of the given generators uniformly.
 |||
 ||| All the given generators are treated as independent, i.e. `oneOf [oneOf [a, b], c]` is not the same as `oneOf [a, b, c]`.
@@ -449,9 +573,7 @@ oneOf : {em : _} ->
         (0 _ : IfUnsolved alem em) =>
         (0 _ : IfUnsolved altsNe $ em /= MaybeEmpty) =>
         GenAlternatives altsNe alem a -> Gen em a
-oneOf {em=NonEmpty} @{nw} @{NT} = mkOneOf @{%search} @{transitive nw %search} . unGenAlts
-oneOf {em=MaybeEmptyDeep} @{_} @{DT} = mkOneOf . unGenAlts
-oneOf {em=MaybeEmpty} = maybe Empty (OneOf {alem=MaybeEmptyDeep}) . strengthen . mapMaybe strengthen
+oneOf = mkOneOf . unGenAlts
 
 ||| Choose one of the given generators with probability proportional to the given value, treating all source generators independently.
 |||
@@ -480,9 +602,7 @@ elements : {em : _} ->
 elements = oneOf {alem=NonEmpty} . altsFromList
 
 export %inline
-elements' : Foldable f =>
-            (0 _ : IfUnsolved f List) =>
-            f a -> Gen0 a
+elements' : Foldable f => (0 _ : IfUnsolved f List) => f a -> Gen0 a
 elements' xs = elements $ fromList $ toList xs
 
 ------------------------------
@@ -500,10 +620,18 @@ elements' xs = elements $ fromList $ toList xs
 ||| `alternativesof $ oneOf gs` must be equivalent to `gs`.
 export
 alternativesOf : Gen em a -> GenAlternatives True em a
+0 alternativesOfNonEmpty : {g : Gen em a} -> IsNonEmpty g => All IsNonEmpty $ alternativesOf g
+
 alternativesOf $ OneOf oo     = mapOneOf oo relax
-alternativesOf $ Labelled l x = processAlternatives (label l) $ alternativesOf x
+alternativesOf $ Labelled l x = mapOneOfElem (alternativesOf x) $ \g, e => Labelled l g @{indexAll e alternativesOfNonEmpty}
 alternativesOf g              = [g]
 
+alternativesOfNonEmpty {g=Pure _}        = [Oh]
+alternativesOfNonEmpty {g=Raw _}         = [Oh]
+alternativesOfNonEmpty {g=OneOf @{ne} _} = allMapOneOf $ \e => relaxNonEmpty @{indexAll e ne}
+alternativesOfNonEmpty {g=Bind _ _}      = [Oh]
+alternativesOfNonEmpty {g=Labelled _ _}  = allMapOneOfElem $ \_ => Oh
+
 ||| Any depth alternatives fetching.
 |||
 ||| Alternatives of depth `0` are meant to be a single-item alternatives list with the original generator,
@@ -522,17 +650,18 @@ deepAlternativesOf (S k) gen = processAlternatives' alternativesOf $ deepAlterna
 |||
 ||| Please notice that this function does NOT influence to the result of `deepAlternativesOf`, if depth is increased by 1.
 export
-forgetAlternatives : {em : _} -> Gen em a -> Gen em a
-forgetAlternatives g@(OneOf {}) = case canBeNotImmediatelyEmpty em of
-  Right _   => single g
-  Left Refl => maybe Empty single $ strengthen {em=MaybeEmptyDeep} g
-  where
-    %inline single : (0 _ : iem `NoWeaker` MaybeEmptyDeep) => (0 _ : iem `NoWeaker` em) => Gen iem a -> Gen em a
-    single g = label "forgetAlternatives" $ OneOf $ MkGenAlts [(1, g)]
-    -- `mkOneOf` is not used here intentionally, since mkOneOf can potentially change the shape of produced tree, but we
-    -- still want precisely this shape here.
-forgetAlternatives (Labelled l x) = label l $ forgetAlternatives x
-forgetAlternatives g = g
+forgetAlternatives : Gen em a -> Gen em a
+0 forgetAlternativesNonEmpty : {g : Gen iem a} -> IsNonEmpty g => IsNonEmpty $ forgetAlternatives g
+
+forgetAlternatives g@(OneOf {})   = Labelled "forgetAlternatives" $ OneOf $ MkGenAlts [(1, g)]
+forgetAlternatives $ Labelled l x = Labelled @{forgetAlternativesNonEmpty} l $ forgetAlternatives x
+forgetAlternatives g              = g
+
+forgetAlternativesNonEmpty {g=Pure _}       = Oh
+forgetAlternativesNonEmpty {g=Raw _}        = Oh
+forgetAlternativesNonEmpty {g=OneOf _}      = Oh
+forgetAlternativesNonEmpty {g=Bind _ _}     = Oh
+forgetAlternativesNonEmpty {g=Labelled _ _} = Oh
 
 ||| Returns generator with internal structure hidden to anything, including combinators,
 ||| except for an empty generator, which would still be returned as an empty generator.
@@ -548,11 +677,10 @@ forgetAlternatives g = g
 ||| being applied to the result of this function.
 export
 forgetStructure : {em : _} -> Gen em a -> Gen em a
-forgetStructure Empty     = Empty
-forgetStructure g@(Raw _) = g
-forgetStructure g with (canBeEmpty em)
-  _ | Right _   = MkRawGen (unGen' g) `Bind` maybe Empty Pure
-  _ | Left Refl = Raw $ MkRawGen $ unGen1 g
+forgetStructure Empty             = Empty
+forgetStructure g@(Raw _)         = g
+forgetStructure g {em=NonEmpty}   = Raw $ MkRawGen $ unGen1 g
+forgetStructure g {em=MaybeEmpty} = MkRawGen (unGen' g) `Bind` maybe Empty Pure
 
 public export
 processAlternatives : (Gen em a -> Gen em b) -> Gen em a -> GenAlternatives True em b
@@ -630,9 +758,9 @@ export
 suchThat_withPrf : Gen em a -> (p : a -> Bool) -> Gen0 $ a `Subset` So . p
 suchThat_withPrf g p = mapMaybe lp g where
   lp : a -> Maybe $ a `Subset` So . p
-  lp x with (p x) proof prf
-    _ | True  = Just $ Element x $ eqToSo prf
-    _ | False = Nothing
+  lp x with (@@@ p x)
+    _ | Element True prf = Just $ Element x $ eqToSo prf
+    _ | Element False _  = Nothing
 
 export infixl 4 `suchThat`
 
@@ -661,9 +789,9 @@ retryUntil_withPrf : (p : a -> Bool) -> (Fuel -> Gen em a) -> Fuel -> Gen0 $ a `
 retryUntil_withPrf p f Dry           = f Dry `suchThat_withPrf` p
 retryUntil_withPrf p f fl'@(More fl) = do
   x <- relax $ f fl'
-  case @@ p x of
-    (True ** prf) => pure $ Element x $ eqToSo prf
-    (False ** _)  => retryUntil_withPrf p f fl
+  case @@@ p x of
+    Element True prf => pure $ Element x $ eqToSo prf
+    Element False _  => retryUntil_withPrf p f fl
 
 ||| More elegant version of `suchThat` for fuelled generators.
 |||
@@ -695,11 +823,10 @@ iterate (S n) f = iterate n f . f
 -- TODO to reimplement `variant` to ensure that preserves the structure as far as it can.
 export
 variant : {em : _} -> Nat -> Gen em a -> Gen em a
-variant _ Empty = Empty
-variant Z gen   = gen
-variant n gen with (canBeEmpty em)
-  _ | Right _   = MkRawGen (iterate n independent $ unGen' gen) `Bind` maybe Empty Pure
-  _ | Left Refl = Raw $ MkRawGen $ iterate n independent $ unGen1 gen
+variant _ Empty               = Empty
+variant Z gen                 = gen
+variant n gen {em=NonEmpty}   = Raw $ MkRawGen $ iterate n independent $ unGen1 gen
+variant n gen {em=MaybeEmpty} = MkRawGen (iterate n independent $ unGen' gen) `Bind` maybe Empty Pure
 
 -----------------------------
 --- Particular generators ---
diff --git a/src/Test/DepTyCheck/Gen/Emptiness.idr b/src/Test/DepTyCheck/Gen/Emptiness.idr
index 8ff0b86be..926a2685a 100644
--- a/src/Test/DepTyCheck/Gen/Emptiness.idr
+++ b/src/Test/DepTyCheck/Gen/Emptiness.idr
@@ -10,65 +10,41 @@ import public Language.Implicits.IfUnsolved
 --- The data ---
 
 public export
-data Emptiness = NonEmpty | MaybeEmptyDeep | MaybeEmpty
+data Emptiness = NonEmpty | MaybeEmpty
 
 public export
 Eq Emptiness where
-  NonEmpty       == NonEmpty       = True
-  MaybeEmptyDeep == MaybeEmptyDeep = True
-  MaybeEmpty     == MaybeEmpty     = True
-
-  NonEmpty       == MaybeEmptyDeep = False
-  NonEmpty       == MaybeEmpty     = False
-  MaybeEmptyDeep == NonEmpty       = False
-  MaybeEmptyDeep == MaybeEmpty     = False
-  MaybeEmpty     == NonEmpty       = False
-  MaybeEmpty     == MaybeEmptyDeep = False
+  NonEmpty   == NonEmpty   = True
+  MaybeEmpty == MaybeEmpty = True
+  NonEmpty   == MaybeEmpty = False
+  MaybeEmpty == NonEmpty   = False
 
 --- Order by strength ---
 
 public export
 data NoWeaker : (from, to : Emptiness) -> Type where
-  NN : NonEmpty       `NoWeaker` NonEmpty
-  ND : NonEmpty       `NoWeaker` MaybeEmptyDeep
-  DD : MaybeEmptyDeep `NoWeaker` MaybeEmptyDeep
-  AS : em             `NoWeaker` MaybeEmpty
+  NN : NonEmpty `NoWeaker` NonEmpty
+  AS : em       `NoWeaker` MaybeEmpty
 
 export infix 6 `NoWeaker`
 
-Uninhabited (MaybeEmpty `NoWeaker` MaybeEmptyDeep) where
-  uninhabited _ impossible
-
 Uninhabited (MaybeEmpty `NoWeaker` NonEmpty) where
   uninhabited _ impossible
 
-Uninhabited (MaybeEmptyDeep `NoWeaker` NonEmpty) where
-  uninhabited _ impossible
-
 noWeaker : (from, to : Emptiness) -> Dec $ from `NoWeaker` to
-noWeaker NonEmpty       NonEmpty       = Yes %search
-noWeaker MaybeEmptyDeep NonEmpty       = No uninhabited
-noWeaker MaybeEmpty     NonEmpty       = No uninhabited
-noWeaker NonEmpty       MaybeEmptyDeep = Yes %search
-noWeaker MaybeEmptyDeep MaybeEmptyDeep = Yes %search
-noWeaker MaybeEmpty     MaybeEmptyDeep = No uninhabited
-noWeaker _              MaybeEmpty     = Yes %search
+noWeaker NonEmpty   NonEmpty   = Yes %search
+noWeaker MaybeEmpty NonEmpty   = No uninhabited
+noWeaker _          MaybeEmpty = Yes %search
 
 export
 Reflexive _ NoWeaker where
-  reflexive {x=NonEmpty}       = %search
-  reflexive {x=MaybeEmptyDeep} = %search
-  reflexive {x=MaybeEmpty}     = %search
+  reflexive {x=NonEmpty}   = %search
+  reflexive {x=MaybeEmpty} = %search
 
 export
 transitive' : x `NoWeaker` y -> y `NoWeaker` z -> x `NoWeaker` z
 transitive' NN NN = %search
-transitive' NN ND = %search
 transitive' NN AS = %search
-transitive' ND DD = %search
-transitive' ND AS = %search
-transitive' DD DD = %search
-transitive' DD AS = %search
 transitive' AS AS = %search
 
 export
@@ -78,7 +54,6 @@ Transitive _ NoWeaker where
 export
 Antisymmetric _ NoWeaker where
   antisymmetric NN NN = Refl
-  antisymmetric DD DD = Refl
   antisymmetric AS AS = Refl
 
 export
@@ -89,70 +64,20 @@ PartialOrder _ NoWeaker where
 
 export
 Connex _ NoWeaker where
-  connex {x=NonEmpty}       {y=NonEmpty}       = %search
-  connex {x=MaybeEmpty}     {y=MaybeEmpty}     = %search
-  connex {x=MaybeEmptyDeep} {y=MaybeEmptyDeep} = %search
-
-  connex {x=NonEmpty}       {y=MaybeEmpty}     = %search
-  connex {x=NonEmpty}       {y=MaybeEmptyDeep} = %search
-  connex {x=MaybeEmpty}     {y=NonEmpty}       = %search
-  connex {x=MaybeEmptyDeep} {y=NonEmpty}       = %search
-
-  connex {x=MaybeEmpty}     {y=MaybeEmptyDeep} = %search
-  connex {x=MaybeEmptyDeep} {y=MaybeEmpty}     = %search
+  connex {x=NonEmpty}   {y=NonEmpty}   = %search
+  connex {x=MaybeEmpty} {y=MaybeEmpty} = %search
+  connex {x=NonEmpty}   {y=MaybeEmpty} = %search
+  connex {x=MaybeEmpty} {y=NonEmpty}   = %search
 
 export
 LinearOrder _ NoWeaker where
 
 export
 StronglyConnex _ NoWeaker where
-  order NonEmpty       NonEmpty       = %search
-  order NonEmpty       MaybeEmptyDeep = %search
-  order NonEmpty       MaybeEmpty     = %search
-  order MaybeEmptyDeep NonEmpty       = %search
-  order MaybeEmpty     NonEmpty       = %search
-  order MaybeEmpty     MaybeEmpty     = %search
-  order MaybeEmpty     MaybeEmptyDeep = %search
-  order MaybeEmptyDeep MaybeEmpty     = %search
-  order MaybeEmptyDeep MaybeEmptyDeep = %search
-
-public export
-CanBeEmpty : Emptiness -> Type
-CanBeEmpty em = MaybeEmptyDeep `NoWeaker` em
-
-export
-decCanBeEmpty : (em : _) -> Dec $ CanBeEmpty em
-decCanBeEmpty _ = noWeaker _ _
-
-namespace NonEmpty
-
-  export
-  extractNE : (0 _ : Not $ CanBeEmpty em) -> em = NonEmpty
-  extractNE ncbe = irrelevantEq $ extractNE' ncbe where
-    extractNE' : {em : _} -> Not (CanBeEmpty em) -> em = NonEmpty
-    extractNE' {em=NonEmpty      } _ = Refl
-    extractNE' {em=MaybeEmptyDeep} f = absurd %search
-    extractNE' {em=MaybeEmpty    } f = absurd %search
-
-export
-canBeEmpty : (em : _) -> Either (em = NonEmpty) (CanBeEmpty em)
-canBeEmpty NonEmpty       = %search
-canBeEmpty MaybeEmptyDeep = %search
-canBeEmpty MaybeEmpty     = %search
-
-public export
-NotImmediatelyEmpty : Emptiness -> Type
-NotImmediatelyEmpty em = em `NoWeaker` MaybeEmptyDeep
-
-export
-canBeNotImmediatelyEmpty : (em : _) -> Either (em = MaybeEmpty) (NotImmediatelyEmpty em)
-canBeNotImmediatelyEmpty NonEmpty       = %search
-canBeNotImmediatelyEmpty MaybeEmptyDeep = %search
-canBeNotImmediatelyEmpty MaybeEmpty     = %search
-
-export
-relaxAnyCanBeEmpty : CanBeEmpty cbe => em `NoWeaker` MaybeEmptyDeep -> em `NoWeaker` cbe
-relaxAnyCanBeEmpty @{cbe} = flip transitive' cbe
+  order NonEmpty   NonEmpty   = %search
+  order NonEmpty   MaybeEmpty = %search
+  order MaybeEmpty NonEmpty   = %search
+  order MaybeEmpty MaybeEmpty = %search
 
 export %hint
 rev : {a, b : _} -> Not (a `NoWeaker` b) -> b `NoWeaker` a
@@ -160,9 +85,8 @@ rev f = either (absurd . f) id $ order a b
 
 export %hint
 nonEmptyIsStrongest : {em : _} -> NonEmpty `NoWeaker` em
-nonEmptyIsStrongest {em=NonEmpty}       = NN
-nonEmptyIsStrongest {em=MaybeEmptyDeep} = ND
-nonEmptyIsStrongest {em=MaybeEmpty}     = AS
+nonEmptyIsStrongest {em=NonEmpty}   = NN
+nonEmptyIsStrongest {em=MaybeEmpty} = AS
 
 export
 maybeEmptyIsMinimal : (0 _ : MaybeEmpty `NoWeaker` x) -> x = MaybeEmpty
@@ -179,40 +103,3 @@ nonEmptyIsMaximal nw = irrelevantEq $ nonEmptyIsMaximal' nw where
 export %hint
 nonEmptyReflexive : {em : _} -> em `NoWeaker` em
 nonEmptyReflexive = reflexive
-
---- Relations for particular generator cases ---
-
--- bind --
-
-public export
-data BindToOuter : (emOfBind, outerEm : Emptiness) -> Type where
-  BTO : (CanBeEmpty biem -> CanBeEmpty em) -> BindToOuter biem em
-
-export %hint
-BindNE : BindToOuter NonEmpty em
-BindNE = BTO $ \case _ impossible
-
-namespace BindToOuter
-
-  export
-  extractNE : (0 _ : BindToOuter em NonEmpty) -> em = NonEmpty
-  extractNE bto = irrelevantEq $ extractNE' bto where
-    extractNE' : {em : _} -> BindToOuter em NonEmpty -> em = NonEmpty
-    extractNE' {em=NonEmpty      } _       = Refl
-    extractNE' {em=MaybeEmptyDeep} $ BTO f = absurd %search
-    extractNE' {em=MaybeEmpty    } $ BTO f = absurd %search
-
-export %hint
-btoRefl : BindToOuter em em
-btoRefl = BTO id
-
-export
-Reflexive _ BindToOuter where
-  reflexive = btoRefl
-
-export
-bindToOuterRelax : x `BindToOuter` y -> y `NoWeaker` z -> x `BindToOuter` z
-bindToOuterRelax f NN = %search
-bindToOuterRelax f ND = %search
-bindToOuterRelax f DD = %search
-bindToOuterRelax f AS = %search