{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Data.List.Relation.Unary.All.Properties.Core where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.List.Relation.Unary.All
import qualified MAlonzo.Code.Data.List.Relation.Unary.Any
import qualified MAlonzo.Code.Function.Bundles
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Negation.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects

-- Data.List.Relation.Unary.All.Properties.Core.¬Any⇒All¬
d_'172'Any'8658'All'172'_38 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  [AgdaAny] ->
  (MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_'172'Any'8658'All'172'_38 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> (T_Any_34 -> T_Irrelevant_20)
-> T_All_44
d_'172'Any'8658'All'172'_38 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 [AgdaAny]
v4 T_Any_34 -> T_Irrelevant_20
v5
  = [AgdaAny] -> (T_Any_34 -> T_Irrelevant_20) -> T_All_44
du_'172'Any'8658'All'172'_38 [AgdaAny]
v4 T_Any_34 -> T_Irrelevant_20
v5
du_'172'Any'8658'All'172'_38 ::
  [AgdaAny] ->
  (MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
du_'172'Any'8658'All'172'_38 :: [AgdaAny] -> (T_Any_34 -> T_Irrelevant_20) -> T_All_44
du_'172'Any'8658'All'172'_38 [AgdaAny]
v0 T_Any_34 -> T_Irrelevant_20
v1
  = case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v0 of
      [] -> T_All_44 -> T_All_44
forall a b. a -> b
coe T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.C_'91''93'_50
      (:) AgdaAny
v2 [AgdaAny]
v3
        -> (AgdaAny -> T_All_44 -> T_All_44)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> T_All_44
forall a b. a -> b
coe
             AgdaAny -> T_All_44 -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.C__'8759'__60
             (\ AgdaAny
v4 ->
                (T_Any_34 -> T_Irrelevant_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_Any_34 -> T_Irrelevant_20
v1 ((AgdaAny -> T_Any_34) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Any_34
MAlonzo.Code.Data.List.Relation.Unary.Any.C_here_46 AgdaAny
v4))
             (([AgdaAny] -> (T_Any_34 -> T_Irrelevant_20) -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> (T_Any_34 -> T_Irrelevant_20) -> T_All_44
du_'172'Any'8658'All'172'_38 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3) AgdaAny
forall a. a
erased)
      [AgdaAny]
_ -> T_All_44
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Unary.All.Properties.Core.All¬⇒¬Any
d_All'172''8658''172'Any_50 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_All'172''8658''172'Any_50 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_All_44
-> T_Any_34
-> T_Irrelevant_20
d_All'172''8658''172'Any_50 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_All_44
-> T_Any_34
-> T_Irrelevant_20
forall a. a
erased
-- Data.List.Relation.Unary.All.Properties.Core.¬All⇒Any¬
d_'172'All'8658'Any'172'_62 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  [AgdaAny] ->
  (MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34
d_'172'All'8658'Any'172'_62 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> (T_All_44 -> T_Irrelevant_20)
-> T_Any_34
d_'172'All'8658'Any'172'_62 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 AgdaAny -> T_Dec_20
v4 [AgdaAny]
v5 ~T_All_44 -> T_Irrelevant_20
v6
  = (AgdaAny -> T_Dec_20) -> [AgdaAny] -> T_Any_34
du_'172'All'8658'Any'172'_62 AgdaAny -> T_Dec_20
v4 [AgdaAny]
v5
du_'172'All'8658'Any'172'_62 ::
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34
du_'172'All'8658'Any'172'_62 :: (AgdaAny -> T_Dec_20) -> [AgdaAny] -> T_Any_34
du_'172'All'8658'Any'172'_62 AgdaAny -> T_Dec_20
v0 [AgdaAny]
v1
  = case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
      []
        -> ((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny -> T_Any_34
forall a b. a -> b
coe
             (AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
             AgdaAny
forall a. a
erased
      (:) AgdaAny
v2 [AgdaAny]
v3
        -> let v4 :: AgdaAny
v4 = (AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v0 AgdaAny
v2 in
           AgdaAny -> T_Any_34
forall a b. a -> b
coe
             (case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
v4 of
                MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v5 T_Reflects_16
v6
                  -> if Bool -> Bool
forall a b. a -> b
coe Bool
v5
                       then (T_Any_34 -> T_Any_34) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_Any_34 -> T_Any_34
MAlonzo.Code.Data.List.Relation.Unary.Any.C_there_54
                              (((AgdaAny -> T_Dec_20) -> [AgdaAny] -> T_Any_34)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T_Dec_20) -> [AgdaAny] -> T_Any_34
du_'172'All'8658'Any'172'_62 ((AgdaAny -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3))
                       else (AgdaAny -> T_Any_34) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> T_Any_34
MAlonzo.Code.Data.List.Relation.Unary.Any.C_here_46
                              ((T_Reflects_16 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v6))
                T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
      [AgdaAny]
_ -> T_Any_34
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Unary.All.Properties.Core.Any¬⇒¬All
d_Any'172''8658''172'All_102 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_Any'172''8658''172'All_102 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> T_Irrelevant_20
d_Any'172''8658''172'All_102 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> T_Irrelevant_20
forall a. a
erased
-- Data.List.Relation.Unary.All.Properties.Core.¬Any↠All¬
d_'172'Any'8608'All'172'_110 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  [AgdaAny] -> MAlonzo.Code.Function.Bundles.T_Surjection_918
d_'172'Any'8608'All'172'_110 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Surjection_918
d_'172'Any'8608'All'172'_110 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 [AgdaAny]
v4
  = [AgdaAny] -> T_Surjection_918
du_'172'Any'8608'All'172'_110 [AgdaAny]
v4
du_'172'Any'8608'All'172'_110 ::
  [AgdaAny] -> MAlonzo.Code.Function.Bundles.T_Surjection_918
du_'172'Any'8608'All'172'_110 :: [AgdaAny] -> T_Surjection_918
du_'172'Any'8608'All'172'_110 [AgdaAny]
v0
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> T_Σ_14) -> T_Surjection_918)
-> AgdaAny -> AgdaAny -> T_Surjection_918
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> T_Σ_14) -> T_Surjection_918
MAlonzo.Code.Function.Bundles.du_mk'8608''8347'_2536
      (([AgdaAny] -> (T_Any_34 -> T_Irrelevant_20) -> T_All_44)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> (T_Any_34 -> T_Irrelevant_20) -> T_All_44
du_'172'Any'8658'All'172'_38 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v0))
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 ->
            (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased))
-- Data.List.Relation.Unary.All.Properties.Core._.to∘from
d_to'8728'from_120 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_to'8728'from_120 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_All_44
-> T__'8801'__12
d_to'8728'from_120 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_All_44
-> T__'8801'__12
forall a. a
erased
-- Data.List.Relation.Unary.All.Properties.Core.Any¬⇔¬All
d_Any'172''8660''172'All_156 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  [AgdaAny] ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
d_Any'172''8660''172'All_156 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> (AgdaAny -> T_Dec_20)
-> T_Equivalence_1858
d_Any'172''8660''172'All_156 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 [AgdaAny]
v4 AgdaAny -> T_Dec_20
v5
  = [AgdaAny] -> (AgdaAny -> T_Dec_20) -> T_Equivalence_1858
du_Any'172''8660''172'All_156 [AgdaAny]
v4 AgdaAny -> T_Dec_20
v5
du_Any'172''8660''172'All_156 ::
  [AgdaAny] ->
  (AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858
du_Any'172''8660''172'All_156 :: [AgdaAny] -> (AgdaAny -> T_Dec_20) -> T_Equivalence_1858
du_Any'172''8660''172'All_156 [AgdaAny]
v0 AgdaAny -> T_Dec_20
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Equivalence_1858)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> T_Equivalence_1858
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_1858
MAlonzo.Code.Function.Bundles.du_mk'8660'_2474 AgdaAny
forall a. a
erased
      (\ AgdaAny
v2 -> ((AgdaAny -> T_Dec_20) -> [AgdaAny] -> T_Any_34)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T_Dec_20) -> [AgdaAny] -> T_Any_34
du_'172'All'8658'Any'172'_62 ((AgdaAny -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v0))
-- Data.List.Relation.Unary.All.Properties.Core._.All-swap
d_All'45'swap_198 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_All'45'swap_198 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> [AgdaAny]
-> T_All_44
-> T_All_44
d_All'45'swap_198 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 [AgdaAny]
v6 [AgdaAny]
v7 T_All_44
v8
  = [AgdaAny] -> [AgdaAny] -> T_All_44 -> T_All_44
du_All'45'swap_198 [AgdaAny]
v6 [AgdaAny]
v7 T_All_44
v8
du_All'45'swap_198 ::
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
du_All'45'swap_198 :: [AgdaAny] -> [AgdaAny] -> T_All_44 -> T_All_44
du_All'45'swap_198 [AgdaAny]
v0 [AgdaAny]
v1 T_All_44
v2
  = case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
      [] -> T_All_44 -> T_All_44
forall a b. a -> b
coe T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.C_'91''93'_50
      (:) AgdaAny
v3 [AgdaAny]
v4
        -> case T_All_44 -> T_All_44
forall a b. a -> b
coe T_All_44
v2 of
             T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.C_'91''93'_50
               -> ((AgdaAny -> AgdaAny) -> [AgdaAny] -> T_All_44)
-> AgdaAny -> AgdaAny -> T_All_44
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny) -> [AgdaAny] -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.du_universal_520
                    ((AgdaAny -> T_All_44) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v5 -> T_All_44
v2)) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1)
             MAlonzo.Code.Data.List.Relation.Unary.All.C__'8759'__60 AgdaAny
v7 T_All_44
v8
               -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v0 of
                    (:) AgdaAny
v9 [AgdaAny]
v10
                      -> case AgdaAny -> T_All_44
forall a b. a -> b
coe AgdaAny
v7 of
                           MAlonzo.Code.Data.List.Relation.Unary.All.C__'8759'__60 AgdaAny
v13 T_All_44
v14
                             -> (AgdaAny -> T_All_44 -> T_All_44) -> AgdaAny -> AgdaAny -> T_All_44
forall a b. a -> b
coe
                                  AgdaAny -> T_All_44 -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.C__'8759'__60
                                  ((AgdaAny -> T_All_44 -> T_All_44) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     AgdaAny -> T_All_44 -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.C__'8759'__60 AgdaAny
v13
                                     (((AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny] -> T_All_44 -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> T_All_44 -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.du_map_164
                                        ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                                           (\ AgdaAny
v15 ->
                                              (T_All_44 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                                                T_All_44 -> AgdaAny
MAlonzo.Code.Data.List.Relation.Unary.All.du_head_114))
                                        ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v10) (T_All_44 -> AgdaAny
forall a b. a -> b
coe T_All_44
v8)))
                                  (([AgdaAny] -> [AgdaAny] -> T_All_44 -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     [AgdaAny] -> [AgdaAny] -> T_All_44 -> T_All_44
du_All'45'swap_198 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v4)
                                     ((AgdaAny -> T_All_44 -> T_All_44) -> T_All_44 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> T_All_44 -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.C__'8759'__60 T_All_44
v14
                                        (((AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny] -> T_All_44 -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> T_All_44 -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.du_map_164
                                           ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                                              (\ AgdaAny
v15 ->
                                                 (T_All_44 -> T_All_44) -> AgdaAny
forall a b. a -> b
coe
                                                   T_All_44 -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.du_tail_116))
                                           ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v10) (T_All_44 -> AgdaAny
forall a b. a -> b
coe T_All_44
v8))))
                           T_All_44
_ -> T_All_44
forall a. a
MAlonzo.RTE.mazUnreachableError
                    [AgdaAny]
_ -> T_All_44
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_All_44
_ -> T_All_44
forall a. a
MAlonzo.RTE.mazUnreachableError
      [AgdaAny]
_ -> T_All_44
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Unary.All.Properties.Core._..generalizedField-P.a
d_'46'generalizedField'45'P'46'a_28211 ::
  T_GeneralizeTel_28219 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'P'46'a_28211 :: T_GeneralizeTel_28219 -> T_Level_18
d_'46'generalizedField'45'P'46'a_28211 T_GeneralizeTel_28219
v0
  = case T_GeneralizeTel_28219 -> T_GeneralizeTel_28219
forall a b. a -> b
coe T_GeneralizeTel_28219
v0 of
      C_mkGeneralizeTel_28221 T_Level_18
v1 T_Level_18
v3 -> T_Level_18 -> T_Level_18
forall a b. a -> b
coe T_Level_18
v1
      T_GeneralizeTel_28219
_ -> T_Level_18
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Unary.All.Properties.Core._..generalizedField-P.A
d_'46'generalizedField'45'P'46'A_28213 ::
  T_GeneralizeTel_28219 -> ()
d_'46'generalizedField'45'P'46'A_28213 :: T_GeneralizeTel_28219 -> T_Level_18
d_'46'generalizedField'45'P'46'A_28213 = T_GeneralizeTel_28219 -> T_Level_18
forall a. a
erased
-- Data.List.Relation.Unary.All.Properties.Core._..generalizedField-P.p
d_'46'generalizedField'45'P'46'p_28215 ::
  T_GeneralizeTel_28219 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'P'46'p_28215 :: T_GeneralizeTel_28219 -> T_Level_18
d_'46'generalizedField'45'P'46'p_28215 T_GeneralizeTel_28219
v0
  = case T_GeneralizeTel_28219 -> T_GeneralizeTel_28219
forall a b. a -> b
coe T_GeneralizeTel_28219
v0 of
      C_mkGeneralizeTel_28221 T_Level_18
v1 T_Level_18
v3 -> T_Level_18 -> T_Level_18
forall a b. a -> b
coe T_Level_18
v3
      T_GeneralizeTel_28219
_ -> T_Level_18
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Unary.All.Properties.Core._..generalizedField-P
d_'46'generalizedField'45'P_28217 ::
  T_GeneralizeTel_28219 -> AgdaAny -> ()
d_'46'generalizedField'45'P_28217 :: T_GeneralizeTel_28219 -> AgdaAny -> T_Level_18
d_'46'generalizedField'45'P_28217 = T_GeneralizeTel_28219 -> AgdaAny -> T_Level_18
forall a. a
erased
-- Data.List.Relation.Unary.All.Properties.Core._.GeneralizeTel
d_GeneralizeTel_28219 :: p -> p -> p -> p -> p -> T_Level_18
d_GeneralizeTel_28219 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
data T_GeneralizeTel_28219
  = C_mkGeneralizeTel_28221 MAlonzo.Code.Agda.Primitive.T_Level_18
                            MAlonzo.Code.Agda.Primitive.T_Level_18