{-# 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 MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Bool
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Algebra.Bundles
import qualified MAlonzo.Code.Algebra.Lattice.Bundles
import qualified MAlonzo.Code.Algebra.Lattice.Properties.BooleanAlgebra
import qualified MAlonzo.Code.Algebra.Lattice.Structures
import qualified MAlonzo.Code.Algebra.Structures
import qualified MAlonzo.Code.Data.Bool.Base
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Function.Bundles
import qualified MAlonzo.Code.Induction.WellFounded
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Definitions
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects

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