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.Data.Bool.Properties where
  
  import Data.Text qualified
  import MAlonzo.Code.Agda.Builtin.Bool qualified
  import MAlonzo.Code.Agda.Builtin.Equality qualified
  import MAlonzo.Code.Agda.Builtin.Sigma qualified
  import MAlonzo.Code.Agda.Builtin.Unit qualified
  import MAlonzo.Code.Agda.Primitive qualified
  import MAlonzo.Code.Algebra.Bundles qualified
  import MAlonzo.Code.Algebra.Lattice.Bundles qualified
  import MAlonzo.Code.Algebra.Lattice.Properties.BooleanAlgebra qualified
  import MAlonzo.Code.Algebra.Lattice.Structures qualified
  import MAlonzo.Code.Algebra.Structures qualified
  import MAlonzo.Code.Data.Bool.Base qualified
  import MAlonzo.Code.Data.Irrelevant qualified
  import MAlonzo.Code.Data.Sum.Base qualified
  import MAlonzo.Code.Function.Bundles qualified
  import MAlonzo.Code.Induction.WellFounded qualified
  import MAlonzo.Code.Relation.Binary.Bundles qualified
  import MAlonzo.Code.Relation.Binary.Definitions qualified
  import MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties qualified
  import MAlonzo.Code.Relation.Binary.Structures qualified
  import MAlonzo.Code.Relation.Nullary.Decidable.Core qualified
  import MAlonzo.Code.Relation.Nullary.Reflects 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
  
  -- Data.Bool.Properties._._Absorbs_
  d__Absorbs__8 ::
    (Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
  d__Absorbs__8 = erased
  -- Data.Bool.Properties._._DistributesOver_
  d__DistributesOver__10 ::
    (Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
  d__DistributesOver__10 = erased
  -- Data.Bool.Properties._._DistributesOverʳ_
  d__DistributesOver'691'__12 ::
    (Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
  d__DistributesOver'691'__12 = erased
  -- Data.Bool.Properties._._DistributesOverˡ_
  d__DistributesOver'737'__14 ::
    (Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
  d__DistributesOver'737'__14 = erased
  -- Data.Bool.Properties._.Absorptive
  d_Absorptive_20 ::
    (Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
  d_Absorptive_20 = erased
  -- Data.Bool.Properties._.Associative
  d_Associative_30 :: (Bool -> Bool -> Bool) -> ()
  d_Associative_30 = erased
  -- Data.Bool.Properties._.Commutative
  d_Commutative_34 :: (Bool -> Bool -> Bool) -> ()
  d_Commutative_34 = erased
  -- Data.Bool.Properties._.Conical
  d_Conical_40 :: Bool -> (Bool -> Bool -> Bool) -> ()
  d_Conical_40 = erased
  -- Data.Bool.Properties._.Idempotent
  d_Idempotent_44 :: (Bool -> Bool -> Bool) -> ()
  d_Idempotent_44 = erased
  -- Data.Bool.Properties._.Identity
  d_Identity_50 :: Bool -> (Bool -> Bool -> Bool) -> ()
  d_Identity_50 = erased
  -- Data.Bool.Properties._.Inverse
  d_Inverse_54 ::
    Bool -> (Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
  d_Inverse_54 = erased
  -- Data.Bool.Properties._.Involutive
  d_Involutive_58 :: (Bool -> Bool) -> ()
  d_Involutive_58 = erased
  -- Data.Bool.Properties._.LeftConical
  d_LeftConical_68 :: Bool -> (Bool -> Bool -> Bool) -> ()
  d_LeftConical_68 = erased
  -- Data.Bool.Properties._.LeftIdentity
  d_LeftIdentity_76 :: Bool -> (Bool -> Bool -> Bool) -> ()
  d_LeftIdentity_76 = erased
  -- Data.Bool.Properties._.LeftInverse
  d_LeftInverse_78 ::
    Bool -> (Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
  d_LeftInverse_78 = erased
  -- Data.Bool.Properties._.LeftZero
  d_LeftZero_84 :: Bool -> (Bool -> Bool -> Bool) -> ()
  d_LeftZero_84 = erased
  -- Data.Bool.Properties._.RightConical
  d_RightConical_98 :: Bool -> (Bool -> Bool -> Bool) -> ()
  d_RightConical_98 = erased
  -- Data.Bool.Properties._.RightIdentity
  d_RightIdentity_106 :: Bool -> (Bool -> Bool -> Bool) -> ()
  d_RightIdentity_106 = erased
  -- Data.Bool.Properties._.RightInverse
  d_RightInverse_108 ::
    Bool -> (Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
  d_RightInverse_108 = erased
  -- Data.Bool.Properties._.RightZero
  d_RightZero_114 :: Bool -> (Bool -> Bool -> Bool) -> ()
  d_RightZero_114 = erased
  -- Data.Bool.Properties._.Selective
  d_Selective_116 :: (Bool -> Bool -> Bool) -> ()
  d_Selective_116 = erased
  -- Data.Bool.Properties._.Zero
  d_Zero_134 :: Bool -> (Bool -> Bool -> Bool) -> ()
  d_Zero_134 = erased
  -- Data.Bool.Properties._.IsBand
  d_IsBand_142 a0 = ()
  -- Data.Bool.Properties._.IsCommutativeMonoid
  d_IsCommutativeMonoid_150 a0 a1 = ()
  -- Data.Bool.Properties._.IsCommutativeSemiring
  d_IsCommutativeSemiring_156 a0 a1 a2 a3 = ()
  -- Data.Bool.Properties._.IsIdempotentCommutativeMonoid
  d_IsIdempotentCommutativeMonoid_164 a0 a1 = ()
  -- Data.Bool.Properties._.IsMagma
  d_IsMagma_182 a0 = ()
  -- Data.Bool.Properties._.IsMonoid
  d_IsMonoid_188 a0 a1 = ()
  -- Data.Bool.Properties._.IsSemigroup
  d_IsSemigroup_210 a0 = ()
  -- Data.Bool.Properties._.IsSemiring
  d_IsSemiring_214 a0 a1 a2 a3 = ()
  -- Data.Bool.Properties._.IsBand.idem
  d_idem_324 ::
    MAlonzo.Code.Algebra.Structures.T_IsBand_508 ->
    Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_idem_324 = erased
  -- Data.Bool.Properties._.IsBand.isSemigroup
  d_isSemigroup_332 ::
    MAlonzo.Code.Algebra.Structures.T_IsBand_508 ->
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
  d_isSemigroup_332 v0
    = coe MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (coe v0)
  -- Data.Bool.Properties._.IsCommutativeMonoid.comm
  d_comm_520 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_736 ->
    Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm_520 = erased
  -- Data.Bool.Properties._.IsCommutativeMonoid.isMonoid
  d_isMonoid_536 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_736 ->
    MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
  d_isMonoid_536 v0
    = coe MAlonzo.Code.Algebra.Structures.d_isMonoid_746 (coe v0)
  -- Data.Bool.Properties._.IsCommutativeSemiring.*-comm
  d_'42''45'comm_720 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemiring_1678 ->
    Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'42''45'comm_720 = erased
  -- Data.Bool.Properties._.IsCommutativeSemiring.isSemiring
  d_isSemiring_790 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemiring_1678 ->
    MAlonzo.Code.Algebra.Structures.T_IsSemiring_1570
  d_isSemiring_790 v0
    = coe MAlonzo.Code.Algebra.Structures.d_isSemiring_1692 (coe v0)
  -- Data.Bool.Properties._.IsIdempotentCommutativeMonoid.idem
  d_idem_968 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_idem_968 = erased
  -- Data.Bool.Properties._.IsIdempotentCommutativeMonoid.isCommutativeMonoid
  d_isCommutativeMonoid_982 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_736
  d_isCommutativeMonoid_982 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862 (coe v0)
  -- Data.Bool.Properties._.IsMagma.isEquivalence
  d_isEquivalence_1482 ::
    MAlonzo.Code.Algebra.Structures.T_IsMagma_176 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
  d_isEquivalence_1482 v0
    = coe MAlonzo.Code.Algebra.Structures.d_isEquivalence_184 (coe v0)
  -- Data.Bool.Properties._.IsMagma.∙-cong
  d_'8729''45'cong_1496 ::
    MAlonzo.Code.Algebra.Structures.T_IsMagma_176 ->
    Bool ->
    Bool ->
    Bool ->
    Bool ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8729''45'cong_1496 = erased
  -- Data.Bool.Properties._.IsMonoid.identity
  d_identity_1592 ::
    MAlonzo.Code.Algebra.Structures.T_IsMonoid_686 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_identity_1592 v0
    = coe MAlonzo.Code.Algebra.Structures.d_identity_698 (coe v0)
  -- Data.Bool.Properties._.IsMonoid.isSemigroup
  d_isSemigroup_1604 ::
    MAlonzo.Code.Algebra.Structures.T_IsMonoid_686 ->
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
  d_isSemigroup_1604 v0
    = coe MAlonzo.Code.Algebra.Structures.d_isSemigroup_696 (coe v0)
  -- Data.Bool.Properties._.IsSemigroup.assoc
  d_assoc_2336 ::
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472 ->
    Bool ->
    Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_assoc_2336 = erased
  -- Data.Bool.Properties._.IsSemigroup.isMagma
  d_isMagma_2340 ::
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472 ->
    MAlonzo.Code.Algebra.Structures.T_IsMagma_176
  d_isMagma_2340 v0
    = coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v0)
  -- Data.Bool.Properties._.IsSemiring.isSemiringWithoutAnnihilatingZero
  d_isSemiringWithoutAnnihilatingZero_2454 ::
    MAlonzo.Code.Algebra.Structures.T_IsSemiring_1570 ->
    MAlonzo.Code.Algebra.Structures.T_IsSemiringWithoutAnnihilatingZero_1468
  d_isSemiringWithoutAnnihilatingZero_2454 v0
    = coe
        MAlonzo.Code.Algebra.Structures.d_isSemiringWithoutAnnihilatingZero_1584
        (coe v0)
  -- Data.Bool.Properties._.IsSemiring.zero
  d_zero_2468 ::
    MAlonzo.Code.Algebra.Structures.T_IsSemiring_1570 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_zero_2468 v0
    = coe MAlonzo.Code.Algebra.Structures.d_zero_1586 (coe v0)
  -- Data.Bool.Properties._.IsBooleanAlgebra
  d_IsBooleanAlgebra_2652 a0 a1 a2 a3 a4 = ()
  -- Data.Bool.Properties._.IsDistributiveLattice
  d_IsDistributiveLattice_2660 a0 a1 = ()
  -- Data.Bool.Properties._.IsLattice
  d_IsLattice_2664 a0 a1 = ()
  -- Data.Bool.Properties._.IsSemilattice
  d_IsSemilattice_2668 :: (Bool -> Bool -> Bool) -> ()
  d_IsSemilattice_2668 = erased
  -- Data.Bool.Properties._.IsBooleanAlgebra.isDistributiveLattice
  d_isDistributiveLattice_2674 ::
    MAlonzo.Code.Algebra.Lattice.Structures.T_IsBooleanAlgebra_3112 ->
    MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3036
  d_isDistributiveLattice_2674 v0
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.d_isDistributiveLattice_3132
        (coe v0)
  -- Data.Bool.Properties._.IsBooleanAlgebra.¬-cong
  d_'172''45'cong_2690 ::
    MAlonzo.Code.Algebra.Lattice.Structures.T_IsBooleanAlgebra_3112 ->
    Bool ->
    Bool ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'172''45'cong_2690 = erased
  -- Data.Bool.Properties._.IsBooleanAlgebra.∧-complement
  d_'8743''45'complement_2698 ::
    MAlonzo.Code.Algebra.Lattice.Structures.T_IsBooleanAlgebra_3112 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'8743''45'complement_2698 v0
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'complement_3136
        (coe v0)
  -- Data.Bool.Properties._.IsBooleanAlgebra.∨-complement
  d_'8744''45'complement_2722 ::
    MAlonzo.Code.Algebra.Lattice.Structures.T_IsBooleanAlgebra_3112 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'8744''45'complement_2722 v0
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'complement_3134
        (coe v0)
  -- Data.Bool.Properties._.IsDistributiveLattice.isLattice
  d_isLattice_2884 ::
    MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3036 ->
    MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962
  d_isLattice_2884 v0
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.d_isLattice_3048 (coe v0)
  -- Data.Bool.Properties._.IsDistributiveLattice.∧-distrib-∨
  d_'8743''45'distrib'45''8744'_2908 ::
    MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3036 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'8743''45'distrib'45''8744'_2908 v0
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'distrib'45''8744'_3052
        (coe v0)
  -- Data.Bool.Properties._.IsDistributiveLattice.∨-distrib-∧
  d_'8744''45'distrib'45''8743'_2926 ::
    MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3036 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'8744''45'distrib'45''8743'_2926 v0
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'distrib'45''8743'_3050
        (coe v0)
  -- Data.Bool.Properties._.IsLattice.absorptive
  d_absorptive_2968 ::
    MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_absorptive_2968 v0
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.d_absorptive_2998 (coe v0)
  -- Data.Bool.Properties._.IsLattice.isEquivalence
  d_isEquivalence_2970 ::
    MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
  d_isEquivalence_2970 v0
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
        (coe v0)
  -- Data.Bool.Properties._.IsLattice.∧-assoc
  d_'8743''45'assoc_2984 ::
    MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
    Bool ->
    Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8743''45'assoc_2984 = erased
  -- Data.Bool.Properties._.IsLattice.∧-comm
  d_'8743''45'comm_2986 ::
    MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
    Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8743''45'comm_2986 = erased
  -- Data.Bool.Properties._.IsLattice.∧-cong
  d_'8743''45'cong_2988 ::
    MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
    Bool ->
    Bool ->
    Bool ->
    Bool ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8743''45'cong_2988 = erased
  -- Data.Bool.Properties._.IsLattice.∨-assoc
  d_'8744''45'assoc_2996 ::
    MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
    Bool ->
    Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8744''45'assoc_2996 = erased
  -- Data.Bool.Properties._.IsLattice.∨-comm
  d_'8744''45'comm_2998 ::
    MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
    Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8744''45'comm_2998 = erased
  -- Data.Bool.Properties._.IsLattice.∨-cong
  d_'8744''45'cong_3000 ::
    MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
    Bool ->
    Bool ->
    Bool ->
    Bool ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8744''45'cong_3000 = erased
  -- Data.Bool.Properties._≟_
  d__'8799'__3082 ::
    Bool ->
    Bool -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  d__'8799'__3082 v0 v1
    = if coe v0
        then if coe v1
               then coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe v1)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 erased)
               else coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe v1) (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
        else (if coe v1
                then coe
                       MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                       (coe v0) (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
                else coe
                       MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                       (coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                       (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 erased))
  -- Data.Bool.Properties.≡-setoid
  d_'8801''45'setoid_3084 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
  d_'8801''45'setoid_3084
    = coe
        MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402
  -- Data.Bool.Properties.≡-decSetoid
  d_'8801''45'decSetoid_3086 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
  d_'8801''45'decSetoid_3086
    = coe
        MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_decSetoid_406
        (coe d__'8799'__3082)
  -- Data.Bool.Properties.≤-reflexive
  d_'8804''45'reflexive_3088 ::
    Bool ->
    Bool ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Data.Bool.Base.T__'8804'__10
  d_'8804''45'reflexive_3088 ~v0 ~v1 ~v2
    = du_'8804''45'reflexive_3088
  du_'8804''45'reflexive_3088 ::
    MAlonzo.Code.Data.Bool.Base.T__'8804'__10
  du_'8804''45'reflexive_3088
    = coe MAlonzo.Code.Data.Bool.Base.C_b'8804'b_16
  -- Data.Bool.Properties.≤-refl
  d_'8804''45'refl_3090 ::
    Bool -> MAlonzo.Code.Data.Bool.Base.T__'8804'__10
  d_'8804''45'refl_3090 ~v0 = du_'8804''45'refl_3090
  du_'8804''45'refl_3090 :: MAlonzo.Code.Data.Bool.Base.T__'8804'__10
  du_'8804''45'refl_3090 = coe du_'8804''45'reflexive_3088
  -- Data.Bool.Properties.≤-trans
  d_'8804''45'trans_3092 ::
    Bool ->
    Bool ->
    Bool ->
    MAlonzo.Code.Data.Bool.Base.T__'8804'__10 ->
    MAlonzo.Code.Data.Bool.Base.T__'8804'__10 ->
    MAlonzo.Code.Data.Bool.Base.T__'8804'__10
  d_'8804''45'trans_3092 ~v0 ~v1 ~v2 v3 v4
    = du_'8804''45'trans_3092 v3 v4
  du_'8804''45'trans_3092 ::
    MAlonzo.Code.Data.Bool.Base.T__'8804'__10 ->
    MAlonzo.Code.Data.Bool.Base.T__'8804'__10 ->
    MAlonzo.Code.Data.Bool.Base.T__'8804'__10
  du_'8804''45'trans_3092 v0 v1
    = case coe v0 of
        MAlonzo.Code.Data.Bool.Base.C_f'8804't_12
          -> coe seq (coe v1) (coe v0)
        MAlonzo.Code.Data.Bool.Base.C_b'8804'b_16 -> coe v1
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.Bool.Properties.≤-antisym
  d_'8804''45'antisym_3096 ::
    Bool ->
    Bool ->
    MAlonzo.Code.Data.Bool.Base.T__'8804'__10 ->
    MAlonzo.Code.Data.Bool.Base.T__'8804'__10 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8804''45'antisym_3096 = erased
  -- Data.Bool.Properties.≤-minimum
  d_'8804''45'minimum_3098 ::
    Bool -> MAlonzo.Code.Data.Bool.Base.T__'8804'__10
  d_'8804''45'minimum_3098 v0
    = if coe v0
        then coe MAlonzo.Code.Data.Bool.Base.C_f'8804't_12
        else coe MAlonzo.Code.Data.Bool.Base.C_b'8804'b_16
  -- Data.Bool.Properties.≤-maximum
  d_'8804''45'maximum_3100 ::
    Bool -> MAlonzo.Code.Data.Bool.Base.T__'8804'__10
  d_'8804''45'maximum_3100 v0
    = if coe v0
        then coe MAlonzo.Code.Data.Bool.Base.C_b'8804'b_16
        else coe MAlonzo.Code.Data.Bool.Base.C_f'8804't_12
  -- Data.Bool.Properties.≤-total
  d_'8804''45'total_3102 ::
    Bool -> Bool -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
  d_'8804''45'total_3102 v0 v1
    = if coe v0
        then coe
               MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
               (coe d_'8804''45'maximum_3100 (coe v1))
        else coe
               MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
               (coe d_'8804''45'minimum_3098 (coe v1))
  -- Data.Bool.Properties._≤?_
  d__'8804''63'__3108 ::
    Bool ->
    Bool -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  d__'8804''63'__3108 v0 v1
    = if coe v0
        then if coe v1
               then coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe v1)
                      (coe
                         MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
                         (coe MAlonzo.Code.Data.Bool.Base.C_b'8804'b_16))
               else coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe v1) (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
        else coe
               MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
               (coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
               (coe
                  MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
                  (coe d_'8804''45'minimum_3098 (coe v1)))
  -- Data.Bool.Properties.≤-irrelevant
  d_'8804''45'irrelevant_3112 ::
    Bool ->
    Bool ->
    MAlonzo.Code.Data.Bool.Base.T__'8804'__10 ->
    MAlonzo.Code.Data.Bool.Base.T__'8804'__10 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8804''45'irrelevant_3112 = erased
  -- Data.Bool.Properties.≤-isPreorder
  d_'8804''45'isPreorder_3114 ::
    MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
  d_'8804''45'isPreorder_3114
    = coe
        MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_4003
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
        (\ v0 v1 v2 -> coe du_'8804''45'reflexive_3088)
        (\ v0 v1 v2 v3 v4 -> coe du_'8804''45'trans_3092 v3 v4)
  -- Data.Bool.Properties.≤-isPartialOrder
  d_'8804''45'isPartialOrder_3116 ::
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
  d_'8804''45'isPartialOrder_3116
    = coe
        MAlonzo.Code.Relation.Binary.Structures.C_IsPartialOrder'46'constructor_9853
        (coe d_'8804''45'isPreorder_3114) erased
  -- Data.Bool.Properties.≤-isTotalOrder
  d_'8804''45'isTotalOrder_3118 ::
    MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_404
  d_'8804''45'isTotalOrder_3118
    = coe
        MAlonzo.Code.Relation.Binary.Structures.C_IsTotalOrder'46'constructor_20555
        (coe d_'8804''45'isPartialOrder_3116) (coe d_'8804''45'total_3102)
  -- Data.Bool.Properties.≤-isDecTotalOrder
  d_'8804''45'isDecTotalOrder_3120 ::
    MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_460
  d_'8804''45'isDecTotalOrder_3120
    = coe
        MAlonzo.Code.Relation.Binary.Structures.C_IsDecTotalOrder'46'constructor_22695
        (coe d_'8804''45'isTotalOrder_3118) (coe d__'8799'__3082)
        (coe d__'8804''63'__3108)
  -- Data.Bool.Properties.≤-poset
  d_'8804''45'poset_3122 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314
  d_'8804''45'poset_3122
    = coe
        MAlonzo.Code.Relation.Binary.Bundles.C_Poset'46'constructor_6389
        d_'8804''45'isPartialOrder_3116
  -- Data.Bool.Properties.≤-preorder
  d_'8804''45'preorder_3124 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
  d_'8804''45'preorder_3124
    = coe
        MAlonzo.Code.Relation.Binary.Bundles.C_Preorder'46'constructor_2267
        d_'8804''45'isPreorder_3114
  -- Data.Bool.Properties.≤-totalOrder
  d_'8804''45'totalOrder_3126 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764
  d_'8804''45'totalOrder_3126
    = coe
        MAlonzo.Code.Relation.Binary.Bundles.C_TotalOrder'46'constructor_15747
        d_'8804''45'isTotalOrder_3118
  -- Data.Bool.Properties.≤-decTotalOrder
  d_'8804''45'decTotalOrder_3128 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_DecTotalOrder_866
  d_'8804''45'decTotalOrder_3128
    = coe
        MAlonzo.Code.Relation.Binary.Bundles.C_DecTotalOrder'46'constructor_17849
        d_'8804''45'isDecTotalOrder_3120
  -- Data.Bool.Properties.<-irrefl
  d_'60''45'irrefl_3130 ::
    Bool ->
    Bool ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Data.Bool.Base.T__'60'__18 ->
    MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
  d_'60''45'irrefl_3130 = erased
  -- Data.Bool.Properties.<-asym
  d_'60''45'asym_3132 ::
    Bool ->
    Bool ->
    MAlonzo.Code.Data.Bool.Base.T__'60'__18 ->
    MAlonzo.Code.Data.Bool.Base.T__'60'__18 ->
    MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
  d_'60''45'asym_3132 = erased
  -- Data.Bool.Properties.<-trans
  d_'60''45'trans_3134 ::
    Bool ->
    Bool ->
    Bool ->
    MAlonzo.Code.Data.Bool.Base.T__'60'__18 ->
    MAlonzo.Code.Data.Bool.Base.T__'60'__18 ->
    MAlonzo.Code.Data.Bool.Base.T__'60'__18
  d_'60''45'trans_3134 = erased
  -- Data.Bool.Properties.<-transʳ
  d_'60''45'trans'691'_3136 ::
    Bool ->
    Bool ->
    Bool ->
    MAlonzo.Code.Data.Bool.Base.T__'8804'__10 ->
    MAlonzo.Code.Data.Bool.Base.T__'60'__18 ->
    MAlonzo.Code.Data.Bool.Base.T__'60'__18
  d_'60''45'trans'691'_3136 = erased
  -- Data.Bool.Properties.<-transˡ
  d_'60''45'trans'737'_3138 ::
    Bool ->
    Bool ->
    Bool ->
    MAlonzo.Code.Data.Bool.Base.T__'60'__18 ->
    MAlonzo.Code.Data.Bool.Base.T__'8804'__10 ->
    MAlonzo.Code.Data.Bool.Base.T__'60'__18
  d_'60''45'trans'737'_3138 = erased
  -- Data.Bool.Properties.<-cmp
  d_'60''45'cmp_3140 ::
    Bool -> Bool -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_158
  d_'60''45'cmp_3140 v0 v1
    = if coe v0
        then if coe v1
               then coe
                      MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_180 erased
               else coe
                      MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_188 erased
        else (if coe v1
                then coe
                       MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_172 erased
                else coe
                       MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_180 erased)
  -- Data.Bool.Properties._<?_
  d__'60''63'__3142 ::
    Bool ->
    Bool -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  d__'60''63'__3142 v0 v1
    = if coe v0
        then coe
               MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
               (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
               (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
        else (if coe v1
                then coe
                       MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                       (coe v1)
                       (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 erased)
                else coe
                       MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                       (coe v1)
                       (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
  -- Data.Bool.Properties.<-resp₂-≡
  d_'60''45'resp'8322''45''8801'_3144 ::
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'60''45'resp'8322''45''8801'_3144
    = coe
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
        (coe (\ v0 v1 v2 v3 v4 -> v4)) (coe (\ v0 v1 v2 v3 v4 -> v4))
  -- Data.Bool.Properties.<-irrelevant
  d_'60''45'irrelevant_3150 ::
    Bool ->
    Bool ->
    MAlonzo.Code.Data.Bool.Base.T__'60'__18 ->
    MAlonzo.Code.Data.Bool.Base.T__'60'__18 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'60''45'irrelevant_3150 = erased
  -- Data.Bool.Properties.<-wellFounded
  d_'60''45'wellFounded_3152 ::
    Bool -> MAlonzo.Code.Induction.WellFounded.T_Acc_42
  d_'60''45'wellFounded_3152 = erased
  -- Data.Bool.Properties._.<-acc
  d_'60''45'acc_3162 ::
    Bool ->
    Bool ->
    Bool ->
    MAlonzo.Code.Data.Bool.Base.T__'60'__18 ->
    MAlonzo.Code.Induction.WellFounded.T_Acc_42
  d_'60''45'acc_3162 = erased
  -- Data.Bool.Properties.<-isStrictPartialOrder
  d_'60''45'isStrictPartialOrder_3164 ::
    MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290
  d_'60''45'isStrictPartialOrder_3164
    = coe
        MAlonzo.Code.Relation.Binary.Structures.C_IsStrictPartialOrder'46'constructor_14045
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
        erased d_'60''45'resp'8322''45''8801'_3144
  -- Data.Bool.Properties.<-isStrictTotalOrder
  d_'60''45'isStrictTotalOrder_3166 ::
    MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_534
  d_'60''45'isStrictTotalOrder_3166
    = coe
        MAlonzo.Code.Relation.Binary.Structures.C_IsStrictTotalOrder'46'constructor_24953
        (coe d_'60''45'isStrictPartialOrder_3164) (coe d_'60''45'cmp_3140)
  -- Data.Bool.Properties.<-strictPartialOrder
  d_'60''45'strictPartialOrder_3168 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_556
  d_'60''45'strictPartialOrder_3168
    = coe
        MAlonzo.Code.Relation.Binary.Bundles.C_StrictPartialOrder'46'constructor_11097
        d_'60''45'isStrictPartialOrder_3164
  -- Data.Bool.Properties.<-strictTotalOrder
  d_'60''45'strictTotalOrder_3170 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036
  d_'60''45'strictTotalOrder_3170
    = coe
        MAlonzo.Code.Relation.Binary.Bundles.C_StrictTotalOrder'46'constructor_21059
        d_'60''45'isStrictTotalOrder_3166
  -- Data.Bool.Properties.∨-assoc
  d_'8744''45'assoc_3172 ::
    Bool ->
    Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8744''45'assoc_3172 = erased
  -- Data.Bool.Properties.∨-comm
  d_'8744''45'comm_3182 ::
    Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8744''45'comm_3182 = erased
  -- Data.Bool.Properties.∨-identityˡ
  d_'8744''45'identity'737'_3184 ::
    Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8744''45'identity'737'_3184 = erased
  -- Data.Bool.Properties.∨-identityʳ
  d_'8744''45'identity'691'_3186 ::
    Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8744''45'identity'691'_3186 = erased
  -- Data.Bool.Properties.∨-identity
  d_'8744''45'identity_3188 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'8744''45'identity_3188
    = coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased erased
  -- Data.Bool.Properties.∨-zeroˡ
  d_'8744''45'zero'737'_3190 ::
    Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8744''45'zero'737'_3190 = erased
  -- Data.Bool.Properties.∨-zeroʳ
  d_'8744''45'zero'691'_3192 ::
    Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8744''45'zero'691'_3192 = erased
  -- Data.Bool.Properties.∨-zero
  d_'8744''45'zero_3194 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'8744''45'zero_3194
    = coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased erased
  -- Data.Bool.Properties.∨-inverseˡ
  d_'8744''45'inverse'737'_3196 ::
    Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8744''45'inverse'737'_3196 = erased
  -- Data.Bool.Properties.∨-inverseʳ
  d_'8744''45'inverse'691'_3198 ::
    Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8744''45'inverse'691'_3198 = erased
  -- Data.Bool.Properties.∨-inverse
  d_'8744''45'inverse_3202 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'8744''45'inverse_3202
    = coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased erased
  -- Data.Bool.Properties.∨-idem
  d_'8744''45'idem_3204 ::
    Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8744''45'idem_3204 = erased
  -- Data.Bool.Properties.∨-sel
  d_'8744''45'sel_3206 ::
    Bool -> Bool -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
  d_'8744''45'sel_3206 v0 ~v1 = du_'8744''45'sel_3206 v0
  du_'8744''45'sel_3206 ::
    Bool -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
  du_'8744''45'sel_3206 v0
    = if coe v0
        then coe MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 erased
        else coe MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 erased
  -- Data.Bool.Properties.∨-conicalˡ
  d_'8744''45'conical'737'_3212 ::
    Bool ->
    Bool ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8744''45'conical'737'_3212 = erased
  -- Data.Bool.Properties.∨-conicalʳ
  d_'8744''45'conical'691'_3214 ::
    Bool ->
    Bool ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8744''45'conical'691'_3214 = erased
  -- Data.Bool.Properties.∨-conical
  d_'8744''45'conical_3216 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'8744''45'conical_3216
    = coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased erased
  -- Data.Bool.Properties.∨-isMagma
  d_'8744''45'isMagma_3218 ::
    MAlonzo.Code.Algebra.Structures.T_IsMagma_176
  d_'8744''45'isMagma_3218
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsMagma'46'constructor_1867
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
        erased
  -- Data.Bool.Properties.∨-magma
  d_'8744''45'magma_3220 :: MAlonzo.Code.Algebra.Bundles.T_Magma_68
  d_'8744''45'magma_3220
    = coe
        MAlonzo.Code.Algebra.Bundles.C_Magma'46'constructor_1279
        MAlonzo.Code.Data.Bool.Base.d__'8744'__30 d_'8744''45'isMagma_3218
  -- Data.Bool.Properties.∨-isSemigroup
  d_'8744''45'isSemigroup_3222 ::
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
  d_'8744''45'isSemigroup_3222
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsSemigroup'46'constructor_10417
        (coe d_'8744''45'isMagma_3218) erased
  -- Data.Bool.Properties.∨-semigroup
  d_'8744''45'semigroup_3224 ::
    MAlonzo.Code.Algebra.Bundles.T_Semigroup_536
  d_'8744''45'semigroup_3224
    = coe
        MAlonzo.Code.Algebra.Bundles.C_Semigroup'46'constructor_9793
        MAlonzo.Code.Data.Bool.Base.d__'8744'__30
        d_'8744''45'isSemigroup_3222
  -- Data.Bool.Properties.∨-isBand
  d_'8744''45'isBand_3226 ::
    MAlonzo.Code.Algebra.Structures.T_IsBand_508
  d_'8744''45'isBand_3226
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsBand'46'constructor_11205
        (coe d_'8744''45'isSemigroup_3222) erased
  -- Data.Bool.Properties.∨-band
  d_'8744''45'band_3228 :: MAlonzo.Code.Algebra.Bundles.T_Band_596
  d_'8744''45'band_3228
    = coe
        MAlonzo.Code.Algebra.Bundles.C_Band'46'constructor_10881
        MAlonzo.Code.Data.Bool.Base.d__'8744'__30 d_'8744''45'isBand_3226
  -- Data.Bool.Properties.∨-isSemilattice
  d_'8744''45'isSemilattice_3230 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
  d_'8744''45'isSemilattice_3230
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsCommutativeBand'46'constructor_13109
        (coe d_'8744''45'isBand_3226) erased
  -- Data.Bool.Properties.∨-semilattice
  d_'8744''45'semilattice_3232 ::
    MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
  d_'8744''45'semilattice_3232
    = coe
        MAlonzo.Code.Algebra.Lattice.Bundles.C_Semilattice'46'constructor_193
        MAlonzo.Code.Data.Bool.Base.d__'8744'__30
        d_'8744''45'isSemilattice_3230
  -- Data.Bool.Properties.∨-isMonoid
  d_'8744''45'isMonoid_3234 ::
    MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
  d_'8744''45'isMonoid_3234
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsMonoid'46'constructor_15873
        (coe d_'8744''45'isSemigroup_3222) (coe d_'8744''45'identity_3188)
  -- Data.Bool.Properties.∨-isCommutativeMonoid
  d_'8744''45'isCommutativeMonoid_3236 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_736
  d_'8744''45'isCommutativeMonoid_3236
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsCommutativeMonoid'46'constructor_17695
        (coe d_'8744''45'isMonoid_3234) erased
  -- Data.Bool.Properties.∨-commutativeMonoid
  d_'8744''45'commutativeMonoid_3238 ::
    MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962
  d_'8744''45'commutativeMonoid_3238
    = coe
        MAlonzo.Code.Algebra.Bundles.C_CommutativeMonoid'46'constructor_17931
        MAlonzo.Code.Data.Bool.Base.d__'8744'__30
        (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
        d_'8744''45'isCommutativeMonoid_3236
  -- Data.Bool.Properties.∨-isIdempotentCommutativeMonoid
  d_'8744''45'isIdempotentCommutativeMonoid_3240 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852
  d_'8744''45'isIdempotentCommutativeMonoid_3240
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsIdempotentCommutativeMonoid'46'constructor_20685
        (coe d_'8744''45'isCommutativeMonoid_3236) erased
  -- Data.Bool.Properties.∨-idempotentCommutativeMonoid
  d_'8744''45'idempotentCommutativeMonoid_3242 ::
    MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148
  d_'8744''45'idempotentCommutativeMonoid_3242
    = coe
        MAlonzo.Code.Algebra.Bundles.C_IdempotentCommutativeMonoid'46'constructor_21499
        MAlonzo.Code.Data.Bool.Base.d__'8744'__30
        (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
        d_'8744''45'isIdempotentCommutativeMonoid_3240
  -- Data.Bool.Properties.∧-assoc
  d_'8743''45'assoc_3244 ::
    Bool ->
    Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8743''45'assoc_3244 = erased
  -- Data.Bool.Properties.∧-comm
  d_'8743''45'comm_3254 ::
    Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8743''45'comm_3254 = erased
  -- Data.Bool.Properties.∧-identityˡ
  d_'8743''45'identity'737'_3256 ::
    Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8743''45'identity'737'_3256 = erased
  -- Data.Bool.Properties.∧-identityʳ
  d_'8743''45'identity'691'_3258 ::
    Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8743''45'identity'691'_3258 = erased
  -- Data.Bool.Properties.∧-identity
  d_'8743''45'identity_3260 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'8743''45'identity_3260
    = coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased erased
  -- Data.Bool.Properties.∧-zeroˡ
  d_'8743''45'zero'737'_3262 ::
    Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8743''45'zero'737'_3262 = erased
  -- Data.Bool.Properties.∧-zeroʳ
  d_'8743''45'zero'691'_3264 ::
    Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8743''45'zero'691'_3264 = erased
  -- Data.Bool.Properties.∧-zero
  d_'8743''45'zero_3266 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'8743''45'zero_3266
    = coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased erased
  -- Data.Bool.Properties.∧-inverseˡ
  d_'8743''45'inverse'737'_3268 ::
    Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8743''45'inverse'737'_3268 = erased
  -- Data.Bool.Properties.∧-inverseʳ
  d_'8743''45'inverse'691'_3270 ::
    Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8743''45'inverse'691'_3270 = erased
  -- Data.Bool.Properties.∧-inverse
  d_'8743''45'inverse_3274 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'8743''45'inverse_3274
    = coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased erased
  -- Data.Bool.Properties.∧-idem
  d_'8743''45'idem_3276 ::
    Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8743''45'idem_3276 = erased
  -- Data.Bool.Properties.∧-sel
  d_'8743''45'sel_3278 ::
    Bool -> Bool -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
  d_'8743''45'sel_3278 v0 ~v1 = du_'8743''45'sel_3278 v0
  du_'8743''45'sel_3278 ::
    Bool -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
  du_'8743''45'sel_3278 v0
    = if coe v0
        then coe MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 erased
        else coe MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 erased
  -- Data.Bool.Properties.∧-conicalˡ
  d_'8743''45'conical'737'_3284 ::
    Bool ->
    Bool ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8743''45'conical'737'_3284 = erased
  -- Data.Bool.Properties.∧-conicalʳ
  d_'8743''45'conical'691'_3286 ::
    Bool ->
    Bool ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8743''45'conical'691'_3286 = erased
  -- Data.Bool.Properties.∧-conical
  d_'8743''45'conical_3288 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'8743''45'conical_3288
    = coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased erased
  -- Data.Bool.Properties.∧-distribˡ-∨
  d_'8743''45'distrib'737''45''8744'_3290 ::
    Bool ->
    Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8743''45'distrib'737''45''8744'_3290 = erased
  -- Data.Bool.Properties.∧-distribʳ-∨
  d_'8743''45'distrib'691''45''8744'_3300 ::
    Bool ->
    Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8743''45'distrib'691''45''8744'_3300 = erased
  -- Data.Bool.Properties.∧-distrib-∨
  d_'8743''45'distrib'45''8744'_3308 ::
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'8743''45'distrib'45''8744'_3308
    = coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased erased
  -- Data.Bool.Properties.∨-distribˡ-∧
  d_'8744''45'distrib'737''45''8743'_3310 ::
    Bool ->
    Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8744''45'distrib'737''45''8743'_3310 = erased
  -- Data.Bool.Properties.∨-distribʳ-∧
  d_'8744''45'distrib'691''45''8743'_3320 ::
    Bool ->
    Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8744''45'distrib'691''45''8743'_3320 = erased
  -- Data.Bool.Properties.∨-distrib-∧
  d_'8744''45'distrib'45''8743'_3328 ::
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'8744''45'distrib'45''8743'_3328
    = coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased erased
  -- Data.Bool.Properties.∧-abs-∨
  d_'8743''45'abs'45''8744'_3330 ::
    Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8743''45'abs'45''8744'_3330 = erased
  -- Data.Bool.Properties.∨-abs-∧
  d_'8744''45'abs'45''8743'_3336 ::
    Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8744''45'abs'45''8743'_3336 = erased
  -- Data.Bool.Properties.∨-∧-absorptive
  d_'8744''45''8743''45'absorptive_3342 ::
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'8744''45''8743''45'absorptive_3342
    = coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased erased
  -- Data.Bool.Properties.∧-isMagma
  d_'8743''45'isMagma_3344 ::
    MAlonzo.Code.Algebra.Structures.T_IsMagma_176
  d_'8743''45'isMagma_3344
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsMagma'46'constructor_1867
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
        erased
  -- Data.Bool.Properties.∧-magma
  d_'8743''45'magma_3346 :: MAlonzo.Code.Algebra.Bundles.T_Magma_68
  d_'8743''45'magma_3346
    = coe
        MAlonzo.Code.Algebra.Bundles.C_Magma'46'constructor_1279
        MAlonzo.Code.Data.Bool.Base.d__'8743'__24 d_'8743''45'isMagma_3344
  -- Data.Bool.Properties.∧-isSemigroup
  d_'8743''45'isSemigroup_3348 ::
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
  d_'8743''45'isSemigroup_3348
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsSemigroup'46'constructor_10417
        (coe d_'8743''45'isMagma_3344) erased
  -- Data.Bool.Properties.∧-semigroup
  d_'8743''45'semigroup_3350 ::
    MAlonzo.Code.Algebra.Bundles.T_Semigroup_536
  d_'8743''45'semigroup_3350
    = coe
        MAlonzo.Code.Algebra.Bundles.C_Semigroup'46'constructor_9793
        MAlonzo.Code.Data.Bool.Base.d__'8743'__24
        d_'8743''45'isSemigroup_3348
  -- Data.Bool.Properties.∧-isBand
  d_'8743''45'isBand_3352 ::
    MAlonzo.Code.Algebra.Structures.T_IsBand_508
  d_'8743''45'isBand_3352
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsBand'46'constructor_11205
        (coe d_'8743''45'isSemigroup_3348) erased
  -- Data.Bool.Properties.∧-band
  d_'8743''45'band_3354 :: MAlonzo.Code.Algebra.Bundles.T_Band_596
  d_'8743''45'band_3354
    = coe
        MAlonzo.Code.Algebra.Bundles.C_Band'46'constructor_10881
        MAlonzo.Code.Data.Bool.Base.d__'8743'__24 d_'8743''45'isBand_3352
  -- Data.Bool.Properties.∧-isSemilattice
  d_'8743''45'isSemilattice_3356 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
  d_'8743''45'isSemilattice_3356
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsCommutativeBand'46'constructor_13109
        (coe d_'8743''45'isBand_3352) erased
  -- Data.Bool.Properties.∧-semilattice
  d_'8743''45'semilattice_3358 ::
    MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
  d_'8743''45'semilattice_3358
    = coe
        MAlonzo.Code.Algebra.Lattice.Bundles.C_Semilattice'46'constructor_193
        MAlonzo.Code.Data.Bool.Base.d__'8743'__24
        d_'8743''45'isSemilattice_3356
  -- Data.Bool.Properties.∧-isMonoid
  d_'8743''45'isMonoid_3360 ::
    MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
  d_'8743''45'isMonoid_3360
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsMonoid'46'constructor_15873
        (coe d_'8743''45'isSemigroup_3348) (coe d_'8743''45'identity_3260)
  -- Data.Bool.Properties.∧-isCommutativeMonoid
  d_'8743''45'isCommutativeMonoid_3362 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_736
  d_'8743''45'isCommutativeMonoid_3362
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsCommutativeMonoid'46'constructor_17695
        (coe d_'8743''45'isMonoid_3360) erased
  -- Data.Bool.Properties.∧-commutativeMonoid
  d_'8743''45'commutativeMonoid_3364 ::
    MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962
  d_'8743''45'commutativeMonoid_3364
    = coe
        MAlonzo.Code.Algebra.Bundles.C_CommutativeMonoid'46'constructor_17931
        MAlonzo.Code.Data.Bool.Base.d__'8743'__24
        (coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
        d_'8743''45'isCommutativeMonoid_3362
  -- Data.Bool.Properties.∧-isIdempotentCommutativeMonoid
  d_'8743''45'isIdempotentCommutativeMonoid_3366 ::
    MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852
  d_'8743''45'isIdempotentCommutativeMonoid_3366
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsIdempotentCommutativeMonoid'46'constructor_20685
        (coe d_'8743''45'isCommutativeMonoid_3362) erased
  -- Data.Bool.Properties.∧-idempotentCommutativeMonoid
  d_'8743''45'idempotentCommutativeMonoid_3368 ::
    MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148
  d_'8743''45'idempotentCommutativeMonoid_3368
    = coe
        MAlonzo.Code.Algebra.Bundles.C_IdempotentCommutativeMonoid'46'constructor_21499
        MAlonzo.Code.Data.Bool.Base.d__'8743'__24
        (coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
        d_'8743''45'isIdempotentCommutativeMonoid_3366
  -- Data.Bool.Properties.∨-∧-isSemiring
  d_'8744''45''8743''45'isSemiring_3370 ::
    MAlonzo.Code.Algebra.Structures.T_IsSemiring_1570
  d_'8744''45''8743''45'isSemiring_3370
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsSemiring'46'constructor_48071
        (coe
           MAlonzo.Code.Algebra.Structures.C_IsSemiringWithoutAnnihilatingZero'46'constructor_43811
           (coe d_'8744''45'isCommutativeMonoid_3236) erased erased
           (coe d_'8743''45'identity_3260)
           (coe d_'8743''45'distrib'45''8744'_3308))
        (coe d_'8743''45'zero_3266)
  -- Data.Bool.Properties.∨-∧-isCommutativeSemiring
  d_'8744''45''8743''45'isCommutativeSemiring_3372 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemiring_1678
  d_'8744''45''8743''45'isCommutativeSemiring_3372
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsCommutativeSemiring'46'constructor_51895
        (coe d_'8744''45''8743''45'isSemiring_3370) erased
  -- Data.Bool.Properties.∨-∧-commutativeSemiring
  d_'8744''45''8743''45'commutativeSemiring_3374 ::
    MAlonzo.Code.Algebra.Bundles.T_CommutativeSemiring_2446
  d_'8744''45''8743''45'commutativeSemiring_3374
    = coe
        MAlonzo.Code.Algebra.Bundles.C_CommutativeSemiring'46'constructor_44731
        MAlonzo.Code.Data.Bool.Base.d__'8744'__30
        MAlonzo.Code.Data.Bool.Base.d__'8743'__24
        (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
        (coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
        d_'8744''45''8743''45'isCommutativeSemiring_3372
  -- Data.Bool.Properties.∧-∨-isSemiring
  d_'8743''45''8744''45'isSemiring_3376 ::
    MAlonzo.Code.Algebra.Structures.T_IsSemiring_1570
  d_'8743''45''8744''45'isSemiring_3376
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsSemiring'46'constructor_48071
        (coe
           MAlonzo.Code.Algebra.Structures.C_IsSemiringWithoutAnnihilatingZero'46'constructor_43811
           (coe d_'8743''45'isCommutativeMonoid_3362) erased erased
           (coe d_'8744''45'identity_3188)
           (coe d_'8744''45'distrib'45''8743'_3328))
        (coe d_'8744''45'zero_3194)
  -- Data.Bool.Properties.∧-∨-isCommutativeSemiring
  d_'8743''45''8744''45'isCommutativeSemiring_3378 ::
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemiring_1678
  d_'8743''45''8744''45'isCommutativeSemiring_3378
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsCommutativeSemiring'46'constructor_51895
        (coe d_'8743''45''8744''45'isSemiring_3376) erased
  -- Data.Bool.Properties.∧-∨-commutativeSemiring
  d_'8743''45''8744''45'commutativeSemiring_3380 ::
    MAlonzo.Code.Algebra.Bundles.T_CommutativeSemiring_2446
  d_'8743''45''8744''45'commutativeSemiring_3380
    = coe
        MAlonzo.Code.Algebra.Bundles.C_CommutativeSemiring'46'constructor_44731
        MAlonzo.Code.Data.Bool.Base.d__'8743'__24
        MAlonzo.Code.Data.Bool.Base.d__'8744'__30
        (coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
        (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
        d_'8743''45''8744''45'isCommutativeSemiring_3378
  -- Data.Bool.Properties.∨-∧-isLattice
  d_'8744''45''8743''45'isLattice_3382 ::
    MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962
  d_'8744''45''8743''45'isLattice_3382
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.C_IsLattice'46'constructor_36793
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
        erased erased erased erased erased erased
        (coe d_'8744''45''8743''45'absorptive_3342)
  -- Data.Bool.Properties.∨-∧-lattice
  d_'8744''45''8743''45'lattice_3384 ::
    MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500
  d_'8744''45''8743''45'lattice_3384
    = coe
        MAlonzo.Code.Algebra.Lattice.Bundles.C_Lattice'46'constructor_7925
        MAlonzo.Code.Data.Bool.Base.d__'8744'__30
        MAlonzo.Code.Data.Bool.Base.d__'8743'__24
        d_'8744''45''8743''45'isLattice_3382
  -- Data.Bool.Properties.∨-∧-isDistributiveLattice
  d_'8744''45''8743''45'isDistributiveLattice_3386 ::
    MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3036
  d_'8744''45''8743''45'isDistributiveLattice_3386
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.C_IsDistributiveLattice'46'constructor_40943
        (coe d_'8744''45''8743''45'isLattice_3382)
        (coe d_'8744''45'distrib'45''8743'_3328)
        (coe d_'8743''45'distrib'45''8744'_3308)
  -- Data.Bool.Properties.∨-∧-distributiveLattice
  d_'8744''45''8743''45'distributiveLattice_3388 ::
    MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584
  d_'8744''45''8743''45'distributiveLattice_3388
    = coe
        MAlonzo.Code.Algebra.Lattice.Bundles.C_DistributiveLattice'46'constructor_9515
        MAlonzo.Code.Data.Bool.Base.d__'8744'__30
        MAlonzo.Code.Data.Bool.Base.d__'8743'__24
        d_'8744''45''8743''45'isDistributiveLattice_3386
  -- Data.Bool.Properties.∨-∧-isBooleanAlgebra
  d_'8744''45''8743''45'isBooleanAlgebra_3390 ::
    MAlonzo.Code.Algebra.Lattice.Structures.T_IsBooleanAlgebra_3112
  d_'8744''45''8743''45'isBooleanAlgebra_3390
    = coe
        MAlonzo.Code.Algebra.Lattice.Structures.C_IsBooleanAlgebra'46'constructor_44015
        (coe d_'8744''45''8743''45'isDistributiveLattice_3386)
        (coe d_'8744''45'inverse_3202) (coe d_'8743''45'inverse_3274)
        erased
  -- Data.Bool.Properties.∨-∧-booleanAlgebra
  d_'8744''45''8743''45'booleanAlgebra_3392 ::
    MAlonzo.Code.Algebra.Lattice.Bundles.T_BooleanAlgebra_682
  d_'8744''45''8743''45'booleanAlgebra_3392
    = coe
        MAlonzo.Code.Algebra.Lattice.Bundles.C_BooleanAlgebra'46'constructor_11509
        MAlonzo.Code.Data.Bool.Base.d__'8744'__30
        MAlonzo.Code.Data.Bool.Base.d__'8743'__24
        MAlonzo.Code.Data.Bool.Base.d_not_22
        (coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
        (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
        d_'8744''45''8743''45'isBooleanAlgebra_3390
  -- Data.Bool.Properties.not-involutive
  d_not'45'involutive_3394 ::
    Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_not'45'involutive_3394 = erased
  -- Data.Bool.Properties.not-injective
  d_not'45'injective_3400 ::
    Bool ->
    Bool ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_not'45'injective_3400 = erased
  -- Data.Bool.Properties.not-¬
  d_not'45''172'_3410 ::
    Bool ->
    Bool ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
  d_not'45''172'_3410 = erased
  -- Data.Bool.Properties.¬-not
  d_'172''45'not_3416 ::
    Bool ->
    Bool ->
    (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'172''45'not_3416 = erased
  -- Data.Bool.Properties.xor-is-ok
  d_xor'45'is'45'ok_3426 ::
    Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_xor'45'is'45'ok_3426 = erased
  -- Data.Bool.Properties.true-xor
  d_true'45'xor_3434 ::
    Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_true'45'xor_3434 = erased
  -- Data.Bool.Properties.xor-same
  d_xor'45'same_3438 ::
    Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_xor'45'same_3438 = erased
  -- Data.Bool.Properties.not-distribˡ-xor
  d_not'45'distrib'737''45'xor_3444 ::
    Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_not'45'distrib'737''45'xor_3444 = erased
  -- Data.Bool.Properties.not-distribʳ-xor
  d_not'45'distrib'691''45'xor_3454 ::
    Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_not'45'distrib'691''45'xor_3454 = erased
  -- Data.Bool.Properties.xor-assoc
  d_xor'45'assoc_3460 ::
    Bool ->
    Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_xor'45'assoc_3460 = erased
  -- Data.Bool.Properties.xor-comm
  d_xor'45'comm_3470 ::
    Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_xor'45'comm_3470 = erased
  -- Data.Bool.Properties.xor-identityˡ
  d_xor'45'identity'737'_3472 ::
    Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_xor'45'identity'737'_3472 = erased
  -- Data.Bool.Properties.xor-identityʳ
  d_xor'45'identity'691'_3474 ::
    Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_xor'45'identity'691'_3474 = erased
  -- Data.Bool.Properties.xor-identity
  d_xor'45'identity_3476 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_xor'45'identity_3476
    = coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased erased
  -- Data.Bool.Properties.xor-inverseˡ
  d_xor'45'inverse'737'_3478 ::
    Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_xor'45'inverse'737'_3478 = erased
  -- Data.Bool.Properties.xor-inverseʳ
  d_xor'45'inverse'691'_3480 ::
    Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_xor'45'inverse'691'_3480 = erased
  -- Data.Bool.Properties.xor-inverse
  d_xor'45'inverse_3484 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_xor'45'inverse_3484
    = coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased erased
  -- Data.Bool.Properties.∧-distribˡ-xor
  d_'8743''45'distrib'737''45'xor_3486 ::
    Bool ->
    Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8743''45'distrib'737''45'xor_3486 = erased
  -- Data.Bool.Properties.∧-distribʳ-xor
  d_'8743''45'distrib'691''45'xor_3496 ::
    Bool ->
    Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8743''45'distrib'691''45'xor_3496 = erased
  -- Data.Bool.Properties.∧-distrib-xor
  d_'8743''45'distrib'45'xor_3506 ::
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'8743''45'distrib'45'xor_3506
    = coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased erased
  -- Data.Bool.Properties.xor-annihilates-not
  d_xor'45'annihilates'45'not_3512 ::
    Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_xor'45'annihilates'45'not_3512 = erased
  -- Data.Bool.Properties.xor-∧-commutativeRing
  d_xor'45''8743''45'commutativeRing_3518 ::
    MAlonzo.Code.Algebra.Bundles.T_CommutativeRing_4016
  d_xor'45''8743''45'commutativeRing_3518
    = coe
        MAlonzo.Code.Algebra.Lattice.Properties.BooleanAlgebra.du_'8853''45''8743''45'commutativeRing_3706
        (coe d_'8744''45''8743''45'booleanAlgebra_3392)
        (coe MAlonzo.Code.Data.Bool.Base.d__xor__36) erased
  -- Data.Bool.Properties.if-float
  d_if'45'float_3792 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    Bool ->
    AgdaAny ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_if'45'float_3792 = erased
  -- Data.Bool.Properties.T-≡
  d_T'45''8801'_3796 ::
    Bool -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714
  d_T'45''8801'_3796 v0
    = if coe v0
        then coe
               MAlonzo.Code.Function.Bundles.du_mk'8660'_2298 erased
               (let v1 = coe MAlonzo.Code.Agda.Builtin.Unit.C_tt_8 in
                coe (coe (\ v2 -> v1)))
        else coe
               MAlonzo.Code.Function.Bundles.du_mk'8660'_2298 erased erased
  -- Data.Bool.Properties.T-not-≡
  d_T'45'not'45''8801'_3800 ::
    Bool -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714
  d_T'45'not'45''8801'_3800 v0
    = if coe v0
        then coe
               MAlonzo.Code.Function.Bundles.du_mk'8660'_2298 erased erased
        else coe
               MAlonzo.Code.Function.Bundles.du_mk'8660'_2298 erased
               (let v1 = coe MAlonzo.Code.Agda.Builtin.Unit.C_tt_8 in
                coe (coe (\ v2 -> v1)))
  -- Data.Bool.Properties.T-∧
  d_T'45''8743'_3806 ::
    Bool -> Bool -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714
  d_T'45''8743'_3806 v0 v1
    = if coe v0
        then if coe v1
               then coe
                      MAlonzo.Code.Function.Bundles.du_mk'8660'_2298
                      (let v2
                             = coe
                                 MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                 (coe MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
                                 (coe MAlonzo.Code.Agda.Builtin.Unit.C_tt_8) in
                       coe (coe (\ v3 -> v2)))
                      (let v2 = coe MAlonzo.Code.Agda.Builtin.Unit.C_tt_8 in
                       coe (coe (\ v3 -> v2)))
               else coe
                      MAlonzo.Code.Function.Bundles.du_mk'8660'_2298 erased
                      (coe (\ v2 -> MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (coe v2)))
        else coe
               MAlonzo.Code.Function.Bundles.du_mk'8660'_2298 erased
               (coe (\ v2 -> MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (coe v2)))
  -- Data.Bool.Properties.T-∨
  d_T'45''8744'_3812 ::
    Bool -> Bool -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714
  d_T'45''8744'_3812 v0 v1
    = if coe v0
        then coe
               MAlonzo.Code.Function.Bundles.du_mk'8660'_2298
               (coe MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38)
               (let v2 = coe MAlonzo.Code.Agda.Builtin.Unit.C_tt_8 in
                coe (coe (\ v3 -> v2)))
        else (if coe v1
                then coe
                       MAlonzo.Code.Function.Bundles.du_mk'8660'_2298
                       (coe MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42)
                       (let v2 = coe MAlonzo.Code.Agda.Builtin.Unit.C_tt_8 in
                        coe (coe (\ v3 -> v2)))
                else coe
                       MAlonzo.Code.Function.Bundles.du_mk'8660'_2298
                       (coe MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38)
                       (coe
                          MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93'_52 (coe (\ v2 -> v2))
                          (coe (\ v2 -> v2))))
  -- Data.Bool.Properties.T-irrelevant
  d_T'45'irrelevant_3814 ::
    Bool ->
    AgdaAny ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_T'45'irrelevant_3814 = erased
  -- Data.Bool.Properties.T?-diag
  d_T'63''45'diag_3818 :: Bool -> AgdaAny -> AgdaAny
  d_T'63''45'diag_3818 v0
    = coe
        MAlonzo.Code.Relation.Nullary.Decidable.Core.du_fromWitness_140
        (coe
           MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
           (coe v0)
           (coe
              MAlonzo.Code.Relation.Nullary.Reflects.d_T'45'reflects_66
              (coe v0)))
  -- Data.Bool.Properties.⇔→≡
  d_'8660''8594''8801'_3828 ::
    Bool ->
    Bool ->
    Bool ->
    MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8660''8594''8801'_3828 = erased
  -- Data.Bool.Properties.push-function-into-if
  d_push'45'function'45'into'45'if_3842 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    Bool ->
    AgdaAny ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_push'45'function'45'into'45'if_3842 = erased
  