content: {-# 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.Relation.Binary.Reasoning.Syntax where
  
  import Data.Text qualified
  import MAlonzo.Code.Agda.Builtin.Equality qualified
  import MAlonzo.Code.Agda.Primitive qualified
  import MAlonzo.Code.Data.Irrelevant qualified
  import MAlonzo.Code.Relation.Nullary.Decidable.Core qualified
  import MAlonzo.Code.Relation.Nullary.Negation.Core qualified
  import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
                      mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
                      word64ToNat)
  import MAlonzo.RTE qualified
  
  -- Relation.Binary.Reasoning.Syntax.begin-syntax.begin_
  d_begin__46 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_begin__46 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8 v9 v10
    = du_begin__46 v8 v9 v10
  du_begin__46 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_begin__46 v0 v1 v2 = coe v0 v1 v2
  -- Relation.Binary.Reasoning.Syntax.SubRelation
  d_SubRelation_60 a0 a1 a2 a3 a4 a5 = ()
  data T_SubRelation_60
    = C_SubRelation'46'constructor_2989 (AgdaAny ->
                                         AgdaAny ->
                                         AgdaAny ->
                                         MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20)
                                        (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
  -- Relation.Binary.Reasoning.Syntax.SubRelation.S
  d_S_82 :: T_SubRelation_60 -> AgdaAny -> AgdaAny -> ()
  d_S_82 = erased
  -- Relation.Binary.Reasoning.Syntax.SubRelation.IsS
  d_IsS_84 :: T_SubRelation_60 -> AgdaAny -> AgdaAny -> AgdaAny -> ()
  d_IsS_84 = erased
  -- Relation.Binary.Reasoning.Syntax.SubRelation.IsS?
  d_IsS'63'_88 ::
    T_SubRelation_60 ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  d_IsS'63'_88 v0
    = case coe v0 of
        C_SubRelation'46'constructor_2989 v3 v4 -> coe v3
        _                                       -> MAlonzo.RTE.mazUnreachableError
  -- Relation.Binary.Reasoning.Syntax.SubRelation.extract
  d_extract_92 ::
    T_SubRelation_60 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_extract_92 v0
    = case coe v0 of
        C_SubRelation'46'constructor_2989 v3 v4 -> coe v4
        _                                       -> MAlonzo.RTE.mazUnreachableError
  -- Relation.Binary.Reasoning.Syntax.begin-subrelation-syntax._.IsS
  d_IsS_110 ::
    T_SubRelation_60 -> AgdaAny -> AgdaAny -> AgdaAny -> ()
  d_IsS_110 = erased
  -- Relation.Binary.Reasoning.Syntax.begin-subrelation-syntax._.IsS?
  d_IsS'63'_112 ::
    T_SubRelation_60 ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  d_IsS'63'_112 v0 = coe d_IsS'63'_88 (coe v0)
  -- Relation.Binary.Reasoning.Syntax.begin-subrelation-syntax._.S
  d_S_114 :: T_SubRelation_60 -> AgdaAny -> AgdaAny -> ()
  d_S_114 = erased
  -- Relation.Binary.Reasoning.Syntax.begin-subrelation-syntax._.extract
  d_extract_116 ::
    T_SubRelation_60 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_extract_116 v0 = coe d_extract_92 (coe v0)
  -- Relation.Binary.Reasoning.Syntax.begin-subrelation-syntax.begin_
  d_begin__126 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    T_SubRelation_60 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_begin__126 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8 v9 ~v10
    = du_begin__126 v6 v7 v8 v9
  du_begin__126 ::
    T_SubRelation_60 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_begin__126 v0 v1 v2 v3
    = coe
        d_extract_92 v0 v1 v2 v3
        (coe
           MAlonzo.Code.Relation.Nullary.Decidable.Core.du_toWitness_134
           (coe d_IsS'63'_88 v0 v1 v2 v3))
  -- Relation.Binary.Reasoning.Syntax.begin-equality-syntax._.begin_
  d_begin__148 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    T_SubRelation_60 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_begin__148 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_begin__148 v6
  du_begin__148 ::
    T_SubRelation_60 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_begin__148 v0 v1 v2 v3 v4 = coe du_begin__126 (coe v0) v1 v2 v3
  -- Relation.Binary.Reasoning.Syntax.begin-apartness-syntax._.begin_
  d_begin__166 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    T_SubRelation_60 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_begin__166 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_begin__166 v6
  du_begin__166 ::
    T_SubRelation_60 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_begin__166 v0 v1 v2 v3 v4 = coe du_begin__126 (coe v0) v1 v2 v3
  -- Relation.Binary.Reasoning.Syntax.begin-strict-syntax._.begin_
  d_begin__184 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    T_SubRelation_60 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_begin__184 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_begin__184 v6
  du_begin__184 ::
    T_SubRelation_60 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_begin__184 v0 v1 v2 v3 v4 = coe du_begin__126 (coe v0) v1 v2 v3
  -- Relation.Binary.Reasoning.Syntax.begin-membership-syntax.step-∈
  d_step'45''8712'_208 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8712'_208 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8 v9 v10 v11
    = du_step'45''8712'_208 v8 v9 v10 v11
  du_step'45''8712'_208 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''8712'_208 v0 v1 v2 v3 = coe v0 v1 v2 v3
  -- Relation.Binary.Reasoning.Syntax.begin-contradiction-syntax._.IsS
  d_IsS_230 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    T_SubRelation_60 ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
    AgdaAny -> AgdaAny -> AgdaAny -> ()
  d_IsS_230 = erased
  -- Relation.Binary.Reasoning.Syntax.begin-contradiction-syntax._.IsS?
  d_IsS'63'_232 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    T_SubRelation_60 ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  d_IsS'63'_232 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 ~v7 = du_IsS'63'_232 v6
  du_IsS'63'_232 ::
    T_SubRelation_60 ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  du_IsS'63'_232 v0 = coe d_IsS'63'_88 (coe v0)
  -- Relation.Binary.Reasoning.Syntax.begin-contradiction-syntax._.S
  d_S_234 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    T_SubRelation_60 ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
    AgdaAny -> AgdaAny -> ()
  d_S_234 = erased
  -- Relation.Binary.Reasoning.Syntax.begin-contradiction-syntax._.extract
  d_extract_236 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    T_SubRelation_60 ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_extract_236 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 ~v7 = du_extract_236 v6
  du_extract_236 ::
    T_SubRelation_60 ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_extract_236 v0 = coe d_extract_92 (coe v0)
  -- Relation.Binary.Reasoning.Syntax.begin-contradiction-syntax.begin-contradiction_
  d_begin'45'contradiction__246 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    T_SubRelation_60 ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny -> MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> AgdaAny
  d_begin'45'contradiction__246 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8
                                ~v9 ~v10 ~v11 ~v12
    = du_begin'45'contradiction__246
  du_begin'45'contradiction__246 :: AgdaAny
  du_begin'45'contradiction__246
    = coe
        MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
        erased
  -- Relation.Binary.Reasoning.Syntax.begin-contradiction-syntax._.x<x
  d_x'60'x_258 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    T_SubRelation_60 ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny -> MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> AgdaAny
  d_x'60'x_258 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 ~v7 v8 v9 ~v10 ~v11 ~v12
    = du_x'60'x_258 v6 v8 v9
  du_x'60'x_258 :: T_SubRelation_60 -> AgdaAny -> AgdaAny -> AgdaAny
  du_x'60'x_258 v0 v1 v2
    = coe
        d_extract_92 v0 v1 v1 v2
        (coe
           MAlonzo.Code.Relation.Nullary.Decidable.Core.du_toWitness_134
           (coe d_IsS'63'_88 v0 v1 v1 v2))
  -- Relation.Binary.Reasoning.Syntax._.forward
  d_forward_290 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_forward_290 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10 ~v11 v12
                v13 v14 v15 v16 v17
    = du_forward_290 v12 v13 v14 v15 v16 v17
  du_forward_290 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_forward_290 v0 v1 v2 v3 v4 v5 = coe v0 v1 v2 v3 v5 v4
  -- Relation.Binary.Reasoning.Syntax._.∼-syntax.step-∼
  d_step'45''8764'_300 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8764'_300 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10
                       ~v11 v12
    = du_step'45''8764'_300 v12
  du_step'45''8764'_300 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''8764'_300 v0 = coe du_forward_290 (coe v0)
  -- Relation.Binary.Reasoning.Syntax._.≲-syntax.step-≲
  d_step'45''8818'_304 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8818'_304 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10
                       ~v11 v12
    = du_step'45''8818'_304 v12
  du_step'45''8818'_304 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''8818'_304 v0 = coe du_forward_290 (coe v0)
  -- Relation.Binary.Reasoning.Syntax._.≤-syntax.step-≤
  d_step'45''8804'_308 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8804'_308 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10
                       ~v11 v12
    = du_step'45''8804'_308 v12
  du_step'45''8804'_308 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''8804'_308 v0 = coe du_forward_290 (coe v0)
  -- Relation.Binary.Reasoning.Syntax._.<-syntax.step-<
  d_step'45''60'_312 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''60'_312 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10
                     ~v11 v12
    = du_step'45''60'_312 v12
  du_step'45''60'_312 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''60'_312 v0 = coe du_forward_290 (coe v0)
  -- Relation.Binary.Reasoning.Syntax._.⊆-syntax.step-⊆
  d_step'45''8838'_316 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8838'_316 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10
                       ~v11 v12
    = du_step'45''8838'_316 v12
  du_step'45''8838'_316 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''8838'_316 v0 = coe du_forward_290 (coe v0)
  -- Relation.Binary.Reasoning.Syntax._.⊂-syntax.step-⊂
  d_step'45''8834'_320 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8834'_320 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10
                       ~v11 v12
    = du_step'45''8834'_320 v12
  du_step'45''8834'_320 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''8834'_320 v0 = coe du_forward_290 (coe v0)
  -- Relation.Binary.Reasoning.Syntax._.⊑-syntax.step-⊑
  d_step'45''8849'_324 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8849'_324 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10
                       ~v11 v12
    = du_step'45''8849'_324 v12
  du_step'45''8849'_324 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''8849'_324 v0 = coe du_forward_290 (coe v0)
  -- Relation.Binary.Reasoning.Syntax._.⊏-syntax.step-⊏
  d_step'45''8847'_328 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8847'_328 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10
                       ~v11 v12
    = du_step'45''8847'_328 v12
  du_step'45''8847'_328 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''8847'_328 v0 = coe du_forward_290 (coe v0)
  -- Relation.Binary.Reasoning.Syntax._.∣-syntax.step-∣
  d_step'45''8739'_332 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8739'_332 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10
                       ~v11 v12
    = du_step'45''8739'_332 v12
  du_step'45''8739'_332 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''8739'_332 v0 = coe du_forward_290 (coe v0)
  -- Relation.Binary.Reasoning.Syntax._.⟶-syntax.step-⟶
  d_step'45''10230'_336 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''10230'_336 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10
                        ~v11 v12
    = du_step'45''10230'_336 v12
  du_step'45''10230'_336 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''10230'_336 v0 = coe du_forward_290 (coe v0)
  -- Relation.Binary.Reasoning.Syntax._.⟶*-syntax.step-⟶*
  d_step'45''10230''42'_340 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''10230''42'_340 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9
                            ~v10 ~v11 v12
    = du_step'45''10230''42'_340 v12
  du_step'45''10230''42'_340 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''10230''42'_340 v0 = coe du_forward_290 (coe v0)
  -- Relation.Binary.Reasoning.Syntax._._.backward
  d_backward_358 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_backward_358 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10 ~v11
                 v12 ~v13 ~v14 v15 v16 v17 v18 v19 v20
    = du_backward_358 v12 v15 v16 v17 v18 v19 v20
  du_backward_358 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_backward_358 v0 v1 v2 v3 v4 v5 v6
    = coe
        du_forward_290 (coe v0) (coe v2) (coe v3) (coe v4) (coe v5)
        (coe v1 v3 v2 v6)
  -- Relation.Binary.Reasoning.Syntax._._.≈-syntax.step-≈-⟩
  d_step'45''8776''45''10217'_368 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8776''45''10217'_368 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8
                                  ~v9 ~v10 ~v11 v12 ~v13 ~v14 ~v15
    = du_step'45''8776''45''10217'_368 v12
  du_step'45''8776''45''10217'_368 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''8776''45''10217'_368 v0 = coe du_forward_290 (coe v0)
  -- Relation.Binary.Reasoning.Syntax._._.≈-syntax.step-≈-⟨
  d_step'45''8776''45''10216'_370 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8776''45''10216'_370 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8
                                  ~v9 ~v10 ~v11 v12 ~v13 ~v14 v15
    = du_step'45''8776''45''10216'_370 v12 v15
  du_step'45''8776''45''10216'_370 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''8776''45''10216'_370 v0 v1
    = coe du_backward_358 (coe v0) (coe v1)
  -- Relation.Binary.Reasoning.Syntax._._.≈-syntax.step-≈
  d_step'45''8776'_372 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8776'_372 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10
                       ~v11 v12 ~v13 ~v14 ~v15
    = du_step'45''8776'_372 v12
  du_step'45''8776'_372 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''8776'_372 v0
    = coe du_step'45''8776''45''10217'_368 (coe v0)
  -- Relation.Binary.Reasoning.Syntax._._.≈-syntax.step-≈˘
  d_step'45''8776''728'_374 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8776''728'_374 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9
                            ~v10 ~v11 v12 ~v13 ~v14 v15
    = du_step'45''8776''728'_374 v12 v15
  du_step'45''8776''728'_374 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''8776''728'_374 v0 v1
    = coe du_step'45''8776''45''10216'_370 (coe v0) (coe v1)
  -- Relation.Binary.Reasoning.Syntax._._.≋-syntax.step-≋-⟩
  d_step'45''8779''45''10217'_378 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8779''45''10217'_378 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8
                                  ~v9 ~v10 ~v11 v12 ~v13 ~v14 ~v15
    = du_step'45''8779''45''10217'_378 v12
  du_step'45''8779''45''10217'_378 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''8779''45''10217'_378 v0 = coe du_forward_290 (coe v0)
  -- Relation.Binary.Reasoning.Syntax._._.≋-syntax.step-≋-⟨
  d_step'45''8779''45''10216'_380 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8779''45''10216'_380 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8
                                  ~v9 ~v10 ~v11 v12 ~v13 ~v14 v15
    = du_step'45''8779''45''10216'_380 v12 v15
  du_step'45''8779''45''10216'_380 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''8779''45''10216'_380 v0 v1
    = coe du_backward_358 (coe v0) (coe v1)
  -- Relation.Binary.Reasoning.Syntax._._.≋-syntax.step-≋
  d_step'45''8779'_382 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8779'_382 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10
                       ~v11 v12 ~v13 ~v14 ~v15
    = du_step'45''8779'_382 v12
  du_step'45''8779'_382 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''8779'_382 v0
    = coe du_step'45''8779''45''10217'_378 (coe v0)
  -- Relation.Binary.Reasoning.Syntax._._.≋-syntax.step-≋˘
  d_step'45''8779''728'_384 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8779''728'_384 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9
                            ~v10 ~v11 v12 ~v13 ~v14 v15
    = du_step'45''8779''728'_384 v12 v15
  du_step'45''8779''728'_384 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''8779''728'_384 v0 v1
    = coe du_step'45''8779''45''10216'_380 (coe v0) (coe v1)
  -- Relation.Binary.Reasoning.Syntax._._.≃-syntax.step-≃-⟩
  d_step'45''8771''45''10217'_388 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8771''45''10217'_388 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8
                                  ~v9 ~v10 ~v11 v12 ~v13 ~v14 ~v15
    = du_step'45''8771''45''10217'_388 v12
  du_step'45''8771''45''10217'_388 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''8771''45''10217'_388 v0 = coe du_forward_290 (coe v0)
  -- Relation.Binary.Reasoning.Syntax._._.≃-syntax.step-≃-⟨
  d_step'45''8771''45''10216'_390 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8771''45''10216'_390 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8
                                  ~v9 ~v10 ~v11 v12 ~v13 ~v14 v15
    = du_step'45''8771''45''10216'_390 v12 v15
  du_step'45''8771''45''10216'_390 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''8771''45''10216'_390 v0 v1
    = coe du_backward_358 (coe v0) (coe v1)
  -- Relation.Binary.Reasoning.Syntax._._.#-syntax.step-#-⟩
  d_step'45''35''45''10217'_394 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''35''45''10217'_394 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8
                                ~v9 ~v10 ~v11 v12 ~v13 ~v14 ~v15
    = du_step'45''35''45''10217'_394 v12
  du_step'45''35''45''10217'_394 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''35''45''10217'_394 v0 = coe du_forward_290 (coe v0)
  -- Relation.Binary.Reasoning.Syntax._._.#-syntax.step-#-⟨
  d_step'45''35''45''10216'_396 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''35''45''10216'_396 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8
                                ~v9 ~v10 ~v11 v12 ~v13 ~v14 v15
    = du_step'45''35''45''10216'_396 v12 v15
  du_step'45''35''45''10216'_396 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''35''45''10216'_396 v0 v1
    = coe du_backward_358 (coe v0) (coe v1)
  -- Relation.Binary.Reasoning.Syntax._._.#-syntax.step-#
  d_step'45''35'_398 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''35'_398 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10
                     ~v11 v12 ~v13 ~v14 ~v15
    = du_step'45''35'_398 v12
  du_step'45''35'_398 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''35'_398 v0
    = coe du_step'45''35''45''10217'_394 (coe v0)
  -- Relation.Binary.Reasoning.Syntax._._.#-syntax.step-#˘
  d_step'45''35''728'_400 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''35''728'_400 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9
                          ~v10 ~v11 v12 ~v13 ~v14 v15
    = du_step'45''35''728'_400 v12 v15
  du_step'45''35''728'_400 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''35''728'_400 v0 v1
    = coe du_step'45''35''45''10216'_396 (coe v0) (coe v1)
  -- Relation.Binary.Reasoning.Syntax._._.⤖-syntax.step-⤖
  d_step'45''10518'_404 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''10518'_404 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10
                        ~v11 v12 ~v13 ~v14 ~v15
    = du_step'45''10518'_404 v12
  du_step'45''10518'_404 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''10518'_404 v0 = coe du_forward_290 (coe v0)
  -- Relation.Binary.Reasoning.Syntax._._.⤖-syntax.step-⬻
  d_step'45''11067'_406 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''11067'_406 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10
                        ~v11 v12 ~v13 ~v14 v15
    = du_step'45''11067'_406 v12 v15
  du_step'45''11067'_406 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''11067'_406 v0 v1
    = coe du_backward_358 (coe v0) (coe v1)
  -- Relation.Binary.Reasoning.Syntax._._.↔-syntax.step-↔-⟩
  d_step'45''8596''45''10217'_410 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8596''45''10217'_410 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8
                                  ~v9 ~v10 ~v11 v12 ~v13 ~v14 ~v15
    = du_step'45''8596''45''10217'_410 v12
  du_step'45''8596''45''10217'_410 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''8596''45''10217'_410 v0 = coe du_forward_290 (coe v0)
  -- Relation.Binary.Reasoning.Syntax._._.↔-syntax.step-↔-⟨
  d_step'45''8596''45''10216'_412 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8596''45''10216'_412 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8
                                  ~v9 ~v10 ~v11 v12 ~v13 ~v14 v15
    = du_step'45''8596''45''10216'_412 v12 v15
  du_step'45''8596''45''10216'_412 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''8596''45''10216'_412 v0 v1
    = coe du_backward_358 (coe v0) (coe v1)
  -- Relation.Binary.Reasoning.Syntax._._.↭-syntax.step-↭-⟩
  d_step'45''8621''45''10217'_416 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8621''45''10217'_416 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8
                                  ~v9 ~v10 ~v11 v12 ~v13 ~v14 ~v15
    = du_step'45''8621''45''10217'_416 v12
  du_step'45''8621''45''10217'_416 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''8621''45''10217'_416 v0 = coe du_forward_290 (coe v0)
  -- Relation.Binary.Reasoning.Syntax._._.↭-syntax.step-↭-⟨
  d_step'45''8621''45''10216'_418 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8621''45''10216'_418 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8
                                  ~v9 ~v10 ~v11 v12 ~v13 ~v14 v15
    = du_step'45''8621''45''10216'_418 v12 v15
  du_step'45''8621''45''10216'_418 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''8621''45''10216'_418 v0 v1
    = coe du_backward_358 (coe v0) (coe v1)
  -- Relation.Binary.Reasoning.Syntax._._.↭-syntax.step-↭
  d_step'45''8621'_420 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8621'_420 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10
                       ~v11 v12 ~v13 ~v14 ~v15
    = du_step'45''8621'_420 v12
  du_step'45''8621'_420 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''8621'_420 v0 = coe du_forward_290 (coe v0)
  -- Relation.Binary.Reasoning.Syntax._._.↭-syntax.step-↭˘
  d_step'45''8621''728'_422 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    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 -> ()) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8621''728'_422 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9
                            ~v10 ~v11 v12 ~v13 ~v14 v15
    = du_step'45''8621''728'_422 v12 v15
  du_step'45''8621''728'_422 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  du_step'45''8621''728'_422 v0 v1
    = coe du_backward_358 (coe v0) (coe v1)
  -- Relation.Binary.Reasoning.Syntax.≡-syntax.step-≡-⟩
  d_step'45''8801''45''10217'_436 ::
    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 ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  d_step'45''8801''45''10217'_436 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_step'45''8801''45''10217'_436 v6
  du_step'45''8801''45''10217'_436 ::
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  du_step'45''8801''45''10217'_436 v0 = coe du_forward_290 (coe v0)
  -- Relation.Binary.Reasoning.Syntax.≡-syntax.step-≡-∣
  d_step'45''8801''45''8739'_442 ::
    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 ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_step'45''8801''45''8739'_442 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8
                                 v9
    = du_step'45''8801''45''8739'_442 v9
  du_step'45''8801''45''8739'_442 :: AgdaAny -> AgdaAny
  du_step'45''8801''45''8739'_442 v0 = coe v0
  -- Relation.Binary.Reasoning.Syntax.≡-syntax.step-≡-⟨
  d_step'45''8801''45''10216'_448 ::
    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 ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  d_step'45''8801''45''10216'_448 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_step'45''8801''45''10216'_448 v6
  du_step'45''8801''45''10216'_448 ::
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  du_step'45''8801''45''10216'_448 v0
    = coe du_backward_358 (coe v0) erased
  -- Relation.Binary.Reasoning.Syntax.≡-syntax.step-≡
  d_step'45''8801'_450 ::
    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 ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  d_step'45''8801'_450 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_step'45''8801'_450 v6
  du_step'45''8801'_450 ::
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  du_step'45''8801'_450 v0
    = coe du_step'45''8801''45''10217'_436 (coe v0)
  -- Relation.Binary.Reasoning.Syntax.≡-syntax.step-≡˘
  d_step'45''8801''728'_452 ::
    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 ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  d_step'45''8801''728'_452 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_step'45''8801''728'_452 v6
  du_step'45''8801''728'_452 ::
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  du_step'45''8801''728'_452 v0
    = coe du_step'45''8801''45''10216'_448 (coe v0)
  -- Relation.Binary.Reasoning.Syntax.≡-noncomputing-syntax.step
  d_step_464 ::
    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 ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    AgdaAny -> AgdaAny
  d_step_464 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 v10
    = du_step_464 v10
  du_step_464 :: AgdaAny -> AgdaAny
  du_step_464 v0 = coe v0
  -- Relation.Binary.Reasoning.Syntax.≡-noncomputing-syntax._.step-≡
  d_step'45''8801'_470 ::
    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 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  d_step'45''8801'_470 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5
    = du_step'45''8801'_470
  du_step'45''8801'_470 ::
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  du_step'45''8801'_470
    = coe du_step'45''8801'_450 (coe (\ v0 v1 v2 v3 v4 -> v4))
  -- Relation.Binary.Reasoning.Syntax.≡-noncomputing-syntax._.step-≡-∣
  d_step'45''8801''45''8739'_472 ::
    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 -> AgdaAny -> AgdaAny
  d_step'45''8801''45''8739'_472 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8
    = du_step'45''8801''45''8739'_472 v8
  du_step'45''8801''45''8739'_472 :: AgdaAny -> AgdaAny
  du_step'45''8801''45''8739'_472 v0 = coe v0
  -- Relation.Binary.Reasoning.Syntax.≡-noncomputing-syntax._.step-≡-⟨
  d_step'45''8801''45''10216'_474 ::
    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 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  d_step'45''8801''45''10216'_474 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5
    = du_step'45''8801''45''10216'_474
  du_step'45''8801''45''10216'_474 ::
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  du_step'45''8801''45''10216'_474
    = coe
        du_step'45''8801''45''10216'_448 (coe (\ v0 v1 v2 v3 v4 -> v4))
  -- Relation.Binary.Reasoning.Syntax.≡-noncomputing-syntax._.step-≡-⟩
  d_step'45''8801''45''10217'_476 ::
    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 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  d_step'45''8801''45''10217'_476 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5
    = du_step'45''8801''45''10217'_476
  du_step'45''8801''45''10217'_476 ::
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  du_step'45''8801''45''10217'_476
    = coe
        du_step'45''8801''45''10217'_436 (coe (\ v0 v1 v2 v3 v4 -> v4))
  -- Relation.Binary.Reasoning.Syntax.≡-noncomputing-syntax._.step-≡˘
  d_step'45''8801''728'_478 ::
    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 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  d_step'45''8801''728'_478 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5
    = du_step'45''8801''728'_478
  du_step'45''8801''728'_478 ::
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
  du_step'45''8801''728'_478
    = coe du_step'45''8801''728'_452 (coe (\ v0 v1 v2 v3 v4 -> v4))
  -- Relation.Binary.Reasoning.Syntax.end-syntax._∎
  d__'8718'_492 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
  d__'8718'_492 ~v0 ~v1 ~v2 ~v3 v4 v5 = du__'8718'_492 v4 v5
  du__'8718'_492 :: (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
  du__'8718'_492 v0 v1 = coe v0 v1
  