{-# 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.Untyped.Relation.Binary.Properties 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.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Untyped
import qualified MAlonzo.Code.Untyped.Relation.Binary.Core

-- Untyped.Relation.Binary.Properties.Reflexive
d_Reflexive_8 ::
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  ()
d_Reflexive_8 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> ()
d_Reflexive_8 = (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> ()
forall a. a
erased
-- Untyped.Relation.Binary.Properties.Transitive
d_Transitive_16 ::
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  ()
d_Transitive_16 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> ()
d_Transitive_16 = (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> ()
forall a. a
erased
-- Untyped.Relation.Binary.Properties.Symmetric
d_Symmetric_28 ::
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  ()
d_Symmetric_28 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> ()
d_Symmetric_28 = (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> ()
forall a. a
erased
-- Untyped.Relation.Binary.Properties.Idempotent
d_Idempotent_38 ::
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  ()
d_Idempotent_38 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> ()
d_Idempotent_38 = (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> ()
forall a. a
erased
-- Untyped.Relation.Binary.Properties._⊆_
d__'8838'__50 ::
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  ()
d__'8838'__50 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> ())
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> ()
d__'8838'__50 = (Integer -> T__'8866'_14 -> T__'8866'_14 -> ())
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> ()
forall a. a
erased
-- Untyped.Relation.Binary.Properties.⊆-trans
d_'8838''45'trans_68 ::
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny -> AgdaAny) ->
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny -> AgdaAny) ->
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny -> AgdaAny
d_'8838''45'trans_68 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> ())
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> ())
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> ())
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny)
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny)
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> AgdaAny
-> AgdaAny
d_'8838''45'trans_68 ~Integer -> T__'8866'_14 -> T__'8866'_14 -> ()
v0 ~Integer -> T__'8866'_14 -> T__'8866'_14 -> ()
v1 ~Integer -> T__'8866'_14 -> T__'8866'_14 -> ()
v2 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v3 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v4 Integer
v5 T__'8866'_14
v6 T__'8866'_14
v7 AgdaAny
v8
  = (Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny)
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny)
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> AgdaAny
-> AgdaAny
du_'8838''45'trans_68 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v3 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v4 Integer
v5 T__'8866'_14
v6 T__'8866'_14
v7 AgdaAny
v8
du_'8838''45'trans_68 ::
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny -> AgdaAny) ->
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny -> AgdaAny) ->
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny -> AgdaAny
du_'8838''45'trans_68 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny)
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny)
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> AgdaAny
-> AgdaAny
du_'8838''45'trans_68 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v0 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v1 Integer
v2 T__'8866'_14
v3 T__'8866'_14
v4 AgdaAny
v5
  = (Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny)
-> Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v1 Integer
v2 T__'8866'_14
v3 T__'8866'_14
v4 ((Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny)
-> Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v0 Integer
v2 T__'8866'_14
v3 T__'8866'_14
v4 AgdaAny
v5)
-- Untyped.Relation.Binary.Properties.Transform
d_Transform_76 :: ()
d_Transform_76 :: ()
d_Transform_76 = ()
forall a. a
erased
-- Untyped.Relation.Binary.Properties.Transform?
d_Transform'63'_80 :: ()
d_Transform'63'_80 :: ()
d_Transform'63'_80 = ()
forall a. a
erased
-- Untyped.Relation.Binary.Properties.Transform₂
d_Transform'8322'_84 :: ()
d_Transform'8322'_84 :: ()
d_Transform'8322'_84 = ()
forall a. a
erased
-- Untyped.Relation.Binary.Properties.Deterministicᵣ
d_Deterministic'7523'_88 ::
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  ()
d_Deterministic'7523'_88 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> ()
d_Deterministic'7523'_88 = (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> ()
forall a. a
erased
-- Untyped.Relation.Binary.Properties.Deterministicₗ
d_Deterministic'8343'_100 ::
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  ()
d_Deterministic'8343'_100 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> ()
d_Deterministic'8343'_100 = (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> ()
forall a. a
erased
-- Untyped.Relation.Binary.Properties.Compatible
d_Compatible_112 ::
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14) ->
  ()
d_Compatible_112 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> ())
-> (Integer -> T__'8866'_14 -> T__'8866'_14) -> ()
d_Compatible_112 = (Integer -> T__'8866'_14 -> T__'8866'_14 -> ())
-> (Integer -> T__'8866'_14 -> T__'8866'_14) -> ()
forall a. a
erased
-- Untyped.Relation.Binary.Properties.Compatible₂
d_Compatible'8322'_124 ::
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14) ->
  ()
d_Compatible'8322'_124 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> ())
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> ()
d_Compatible'8322'_124 = (Integer -> T__'8866'_14 -> T__'8866'_14 -> ())
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> ()
forall a. a
erased
-- Untyped.Relation.Binary.Properties.pointwise-refl
d_pointwise'45'refl_146 ::
  Integer ->
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  (Integer -> MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny) ->
  MAlonzo.Code.Untyped.Relation.Binary.Core.T_Pointwise_20
d_pointwise'45'refl_146 :: Integer
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> ())
-> [T__'8866'_14]
-> (Integer -> T__'8866'_14 -> AgdaAny)
-> T_Pointwise_20
d_pointwise'45'refl_146 Integer
v0 ~Integer -> T__'8866'_14 -> T__'8866'_14 -> ()
v1 [T__'8866'_14]
v2 Integer -> T__'8866'_14 -> AgdaAny
v3
  = Integer
-> [T__'8866'_14]
-> (Integer -> T__'8866'_14 -> AgdaAny)
-> T_Pointwise_20
du_pointwise'45'refl_146 Integer
v0 [T__'8866'_14]
v2 Integer -> T__'8866'_14 -> AgdaAny
v3
du_pointwise'45'refl_146 ::
  Integer ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  (Integer -> MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny) ->
  MAlonzo.Code.Untyped.Relation.Binary.Core.T_Pointwise_20
du_pointwise'45'refl_146 :: Integer
-> [T__'8866'_14]
-> (Integer -> T__'8866'_14 -> AgdaAny)
-> T_Pointwise_20
du_pointwise'45'refl_146 Integer
v0 [T__'8866'_14]
v1 Integer -> T__'8866'_14 -> AgdaAny
v2
  = case [T__'8866'_14] -> [AgdaAny]
forall a b. a -> b
coe [T__'8866'_14]
v1 of
      [] -> T_Pointwise_20 -> T_Pointwise_20
forall a b. a -> b
coe T_Pointwise_20
MAlonzo.Code.Untyped.Relation.Binary.Core.C_'91''93'_26
      (:) AgdaAny
v3 [AgdaAny]
v4
        -> (AgdaAny -> T_Pointwise_20 -> T_Pointwise_20)
-> AgdaAny -> AgdaAny -> T_Pointwise_20
forall a b. a -> b
coe
             AgdaAny -> T_Pointwise_20 -> T_Pointwise_20
MAlonzo.Code.Untyped.Relation.Binary.Core.C__'8759'__36
             ((Integer -> T__'8866'_14 -> AgdaAny)
-> Integer -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> T__'8866'_14 -> AgdaAny
v2 Integer
v0 AgdaAny
v3)
             ((Integer
 -> [T__'8866'_14]
 -> (Integer -> T__'8866'_14 -> AgdaAny)
 -> T_Pointwise_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer
-> [T__'8866'_14]
-> (Integer -> T__'8866'_14 -> AgdaAny)
-> T_Pointwise_20
du_pointwise'45'refl_146 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v4) ((Integer -> T__'8866'_14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe Integer -> T__'8866'_14 -> AgdaAny
v2))
      [AgdaAny]
_ -> T_Pointwise_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.Relation.Binary.Properties.Refines
d_Refines_158 ::
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14) ->
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  ()
d_Refines_158 :: (Integer -> T__'8866'_14 -> T__'8866'_14)
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> ()
d_Refines_158 = (Integer -> T__'8866'_14 -> T__'8866'_14)
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> ()
forall a. a
erased
-- Untyped.Relation.Binary.Properties.Refines?
d_Refines'63'_168 ::
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   Maybe MAlonzo.Code.Untyped.T__'8866'_14) ->
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  ()
d_Refines'63'_168 :: (Integer -> T__'8866'_14 -> Maybe T__'8866'_14)
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> ()
d_Refines'63'_168 = (Integer -> T__'8866'_14 -> Maybe T__'8866'_14)
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> ()
forall a. a
erased
-- Untyped.Relation.Binary.Properties.Refines?-⊆
d_Refines'63''45''8838'_188 ::
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   Maybe MAlonzo.Code.Untyped.T__'8866'_14) ->
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny -> AgdaAny) ->
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny) ->
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_Refines'63''45''8838'_188 :: (Integer -> T__'8866'_14 -> Maybe T__'8866'_14)
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> ())
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> ())
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny)
-> (Integer
    -> T__'8866'_14 -> T__'8866'_14 -> T__'8801'__12 -> AgdaAny)
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8801'__12
-> AgdaAny
d_Refines'63''45''8838'_188 ~Integer -> T__'8866'_14 -> Maybe T__'8866'_14
v0 ~Integer -> T__'8866'_14 -> T__'8866'_14 -> ()
v1 ~Integer -> T__'8866'_14 -> T__'8866'_14 -> ()
v2 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v3 Integer -> T__'8866'_14 -> T__'8866'_14 -> T__'8801'__12 -> AgdaAny
v4 Integer
v5 T__'8866'_14
v6 T__'8866'_14
v7 T__'8801'__12
v8
  = (Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny)
-> (Integer
    -> T__'8866'_14 -> T__'8866'_14 -> T__'8801'__12 -> AgdaAny)
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8801'__12
-> AgdaAny
du_Refines'63''45''8838'_188 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v3 Integer -> T__'8866'_14 -> T__'8866'_14 -> T__'8801'__12 -> AgdaAny
v4 Integer
v5 T__'8866'_14
v6 T__'8866'_14
v7 T__'8801'__12
v8
du_Refines'63''45''8838'_188 ::
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny -> AgdaAny) ->
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny) ->
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
du_Refines'63''45''8838'_188 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny)
-> (Integer
    -> T__'8866'_14 -> T__'8866'_14 -> T__'8801'__12 -> AgdaAny)
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8801'__12
-> AgdaAny
du_Refines'63''45''8838'_188 Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v0 Integer -> T__'8866'_14 -> T__'8866'_14 -> T__'8801'__12 -> AgdaAny
v1 Integer
v2 T__'8866'_14
v3 T__'8866'_14
v4 T__'8801'__12
v5
  = (Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny)
-> Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny
v0 Integer
v2 T__'8866'_14
v3 T__'8866'_14
v4 ((Integer
 -> T__'8866'_14 -> T__'8866'_14 -> T__'8801'__12 -> AgdaAny)
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8801'__12
-> AgdaAny
forall a b. a -> b
coe Integer -> T__'8866'_14 -> T__'8866'_14 -> T__'8801'__12 -> AgdaAny
v1 Integer
v2 T__'8866'_14
v3 T__'8866'_14
v4 T__'8801'__12
v5)
-- Untyped.Relation.Binary.Properties.Refinement?
d_Refinement'63'_196 ::
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  ()
d_Refinement'63'_196 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> ()
d_Refinement'63'_196 = (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> ()
forall a. a
erased
-- Untyped.Relation.Binary.Properties.refine?
d_refine'63'_210 ::
  Integer ->
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  Maybe MAlonzo.Code.Untyped.T__'8866'_14
d_refine'63'_210 :: Integer
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> ())
-> (Integer -> T__'8866'_14 -> Maybe T_Σ_14)
-> T__'8866'_14
-> Maybe T__'8866'_14
d_refine'63'_210 Integer
v0 ~Integer -> T__'8866'_14 -> T__'8866'_14 -> ()
v1 Integer -> T__'8866'_14 -> Maybe T_Σ_14
v2 T__'8866'_14
v3 = Integer
-> (Integer -> T__'8866'_14 -> Maybe T_Σ_14)
-> T__'8866'_14
-> Maybe T__'8866'_14
du_refine'63'_210 Integer
v0 Integer -> T__'8866'_14 -> Maybe T_Σ_14
v2 T__'8866'_14
v3
du_refine'63'_210 ::
  Integer ->
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  Maybe MAlonzo.Code.Untyped.T__'8866'_14
du_refine'63'_210 :: Integer
-> (Integer -> T__'8866'_14 -> Maybe T_Σ_14)
-> T__'8866'_14
-> Maybe T__'8866'_14
du_refine'63'_210 Integer
v0 Integer -> T__'8866'_14 -> Maybe T_Σ_14
v1 T__'8866'_14
v2
  = let v3 :: AgdaAny
v3 = (Integer -> T__'8866'_14 -> Maybe T_Σ_14)
-> Integer -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe Integer -> T__'8866'_14 -> Maybe T_Σ_14
v1 Integer
v0 T__'8866'_14
v2 in
    AgdaAny -> Maybe T__'8866'_14
forall a b. a -> b
coe
      (case AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe AgdaAny
v3 of
         MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v4
           -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v4 of
                MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v5 AgdaAny
v6
                  -> (AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5)
                T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
         Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3
         Maybe AgdaAny
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Untyped.Relation.Binary.Properties.refine?-refines
d_refine'63''45'refines_234 ::
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_refine'63''45'refines_234 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> ())
-> (Integer -> T__'8866'_14 -> Maybe T_Σ_14)
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8801'__12
-> AgdaAny
d_refine'63''45'refines_234 ~Integer -> T__'8866'_14 -> T__'8866'_14 -> ()
v0 Integer -> T__'8866'_14 -> Maybe T_Σ_14
v1 Integer
v2 T__'8866'_14
v3 ~T__'8866'_14
v4 ~T__'8801'__12
v5
  = (Integer -> T__'8866'_14 -> Maybe T_Σ_14)
-> Integer -> T__'8866'_14 -> AgdaAny
du_refine'63''45'refines_234 Integer -> T__'8866'_14 -> Maybe T_Σ_14
v1 Integer
v2 T__'8866'_14
v3
du_refine'63''45'refines_234 ::
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  Integer -> MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny
du_refine'63''45'refines_234 :: (Integer -> T__'8866'_14 -> Maybe T_Σ_14)
-> Integer -> T__'8866'_14 -> AgdaAny
du_refine'63''45'refines_234 Integer -> T__'8866'_14 -> Maybe T_Σ_14
v0 Integer
v1 T__'8866'_14
v2
  = let v3 :: AgdaAny
v3 = (Integer -> T__'8866'_14 -> Maybe T_Σ_14)
-> Integer -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe Integer -> T__'8866'_14 -> Maybe T_Σ_14
v0 Integer
v1 T__'8866'_14
v2 in
    AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (case AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe AgdaAny
v3 of
         MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v4
           -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v4 of
                MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v5 AgdaAny
v6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6
                T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
         Maybe AgdaAny
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)