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.Setoid where
  
  import Data.Text qualified
  import MAlonzo.Code.Agda.Builtin.Equality qualified
  import MAlonzo.Code.Agda.Primitive qualified
  import MAlonzo.Code.Relation.Binary.Bundles qualified
  import MAlonzo.Code.Relation.Binary.Reasoning.Base.Single qualified
  import MAlonzo.Code.Relation.Binary.Reasoning.Syntax qualified
  import MAlonzo.Code.Relation.Binary.Structures 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.Setoid.SingleRelReasoning._IsRelatedTo_
  d__IsRelatedTo__38 a0 a1 a2 a3 a4 = ()
  -- Relation.Binary.Reasoning.Setoid.SingleRelReasoning._∎
  d__'8718'_40 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  d__'8718'_40 ~v0 ~v1 v2 = du__'8718'_40 v2
  du__'8718'_40 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  du__'8718'_40 v0
    = let v1
            = MAlonzo.Code.Relation.Binary.Structures.d_refl_34
                (coe
                   MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60
                   (coe v0)) in
      coe
        (coe
           MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
           (coe
              MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_stop_54
              (coe v1)))
  -- Relation.Binary.Reasoning.Setoid.SingleRelReasoning.begin_
  d_begin__42 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    AgdaAny
  d_begin__42 ~v0 ~v1 ~v2 = du_begin__42
  du_begin__42 ::
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    AgdaAny
  du_begin__42
    = coe
        MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
        (\ v0 v1 v2 ->
           coe
             MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_start_36 v2)
  -- Relation.Binary.Reasoning.Setoid.SingleRelReasoning.start
  d_start_46 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    AgdaAny
  d_start_46 ~v0 ~v1 ~v2 = du_start_46
  du_start_46 ::
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    AgdaAny
  du_start_46 v0 v1 v2
    = coe
        MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_start_36 v2
  -- Relation.Binary.Reasoning.Setoid.SingleRelReasoning.step-≡
  d_step'45''8801'_50 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  d_step'45''8801'_50 ~v0 ~v1 ~v2 = du_step'45''8801'_50
  du_step'45''8801'_50 ::
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  du_step'45''8801'_50
    = coe
        MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801'_450
        (coe (\ v0 v1 v2 v3 v4 -> v4))
  -- Relation.Binary.Reasoning.Setoid.SingleRelReasoning.step-≡-∣
  d_step'45''8801''45''8739'_52 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  d_step'45''8801''45''8739'_52 ~v0 ~v1 ~v2 ~v3 ~v4 v5
    = du_step'45''8801''45''8739'_52 v5
  du_step'45''8801''45''8739'_52 ::
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  du_step'45''8801''45''8739'_52 v0 = coe v0
  -- Relation.Binary.Reasoning.Setoid.SingleRelReasoning.step-≡-⟨
  d_step'45''8801''45''10216'_54 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  d_step'45''8801''45''10216'_54 ~v0 ~v1 ~v2
    = du_step'45''8801''45''10216'_54
  du_step'45''8801''45''10216'_54 ::
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  du_step'45''8801''45''10216'_54
    = coe
        MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10216'_448
        (coe (\ v0 v1 v2 v3 v4 -> v4))
  -- Relation.Binary.Reasoning.Setoid.SingleRelReasoning.step-≡-⟩
  d_step'45''8801''45''10217'_56 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  d_step'45''8801''45''10217'_56 ~v0 ~v1 ~v2
    = du_step'45''8801''45''10217'_56
  du_step'45''8801''45''10217'_56 ::
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  du_step'45''8801''45''10217'_56
    = coe
        MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
        (coe (\ v0 v1 v2 v3 v4 -> v4))
  -- Relation.Binary.Reasoning.Setoid.SingleRelReasoning.step-≡˘
  d_step'45''8801''728'_58 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  d_step'45''8801''728'_58 ~v0 ~v1 ~v2 = du_step'45''8801''728'_58
  du_step'45''8801''728'_58 ::
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  du_step'45''8801''728'_58
    = coe
        MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''728'_452
        (coe (\ v0 v1 v2 v3 v4 -> v4))
  -- Relation.Binary.Reasoning.Setoid.SingleRelReasoning.stop
  d_stop_60 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  d_stop_60 ~v0 ~v1 v2 = du_stop_60 v2
  du_stop_60 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  du_stop_60 v0
    = coe
        MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_stop_54
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_refl_34
           (coe
              MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0)))
  -- Relation.Binary.Reasoning.Setoid.SingleRelReasoning.∼-go
  d_'8764''45'go_62 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  d_'8764''45'go_62 ~v0 ~v1 v2 = du_'8764''45'go_62 v2
  du_'8764''45'go_62 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  du_'8764''45'go_62 v0
    = coe
        MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_trans_38
           (coe
              MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0)))
  -- Relation.Binary.Reasoning.Setoid.SingleRelReasoning.≡-go
  d_'8801''45'go_64 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  d_'8801''45'go_64 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 v7
    = du_'8801''45'go_64 v7
  du_'8801''45'go_64 ::
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  du_'8801''45'go_64 v0 = coe v0
  -- Relation.Binary.Reasoning.Setoid._.step-≈
  d_step'45''8776'_72 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  d_step'45''8776'_72 ~v0 ~v1 v2 = du_step'45''8776'_72 v2
  du_step'45''8776'_72 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  du_step'45''8776'_72 v0
    = coe
        MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776'_372
        (coe
           MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
           (coe
              MAlonzo.Code.Relation.Binary.Structures.d_trans_38
              (coe
                 MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0))))
  -- Relation.Binary.Reasoning.Setoid._.step-≈-⟨
  d_step'45''8776''45''10216'_74 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  d_step'45''8776''45''10216'_74 ~v0 ~v1 v2
    = du_step'45''8776''45''10216'_74 v2
  du_step'45''8776''45''10216'_74 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  du_step'45''8776''45''10216'_74 v0
    = coe
        MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10216'_370
        (coe
           MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
           (coe
              MAlonzo.Code.Relation.Binary.Structures.d_trans_38
              (coe
                 MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0))))
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_sym_36
           (coe
              MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0)))
  -- Relation.Binary.Reasoning.Setoid._.step-≈-⟩
  d_step'45''8776''45''10217'_76 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  d_step'45''8776''45''10217'_76 ~v0 ~v1 v2
    = du_step'45''8776''45''10217'_76 v2
  du_step'45''8776''45''10217'_76 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  du_step'45''8776''45''10217'_76 v0
    = coe
        MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_368
        (coe
           MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
           (coe
              MAlonzo.Code.Relation.Binary.Structures.d_trans_38
              (coe
                 MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0))))
  -- Relation.Binary.Reasoning.Setoid._.step-≈˘
  d_step'45''8776''728'_78 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  d_step'45''8776''728'_78 ~v0 ~v1 v2 = du_step'45''8776''728'_78 v2
  du_step'45''8776''728'_78 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26 ->
    AgdaAny ->
    MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.T__IsRelatedTo__26
  du_step'45''8776''728'_78 v0
    = coe
        MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''728'_374
        (coe
           MAlonzo.Code.Relation.Binary.Reasoning.Base.Single.du_'8764''45'go_40
           (coe
              MAlonzo.Code.Relation.Binary.Structures.d_trans_38
              (coe
                 MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0))))
        (coe
           MAlonzo.Code.Relation.Binary.Structures.d_sym_36
           (coe
              MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0)))
  