content: {-# LANGUAGE BangPatterns              #-}
  {-# LANGUAGE EmptyCase                 #-}
  {-# LANGUAGE EmptyDataDecls            #-}
  {-# LANGUAGE ExistentialQuantification #-}
  {-# LANGUAGE NoMonomorphismRestriction #-}
  {-# LANGUAGE OverloadedStrings         #-}
  {-# LANGUAGE PatternSynonyms           #-}
  {-# LANGUAGE RankNTypes                #-}
  {-# LANGUAGE ScopedTypeVariables       #-}
  
  {-# OPTIONS_GHC -Wno-overlapping-patterns #-}
  
  module MAlonzo.Code.Algebra.Consequences.Propositional where
  
  import Data.Text qualified
  import MAlonzo.Code.Agda.Builtin.Equality qualified
  import MAlonzo.Code.Agda.Builtin.Sigma qualified
  import MAlonzo.Code.Agda.Primitive qualified
  import MAlonzo.Code.Algebra.Consequences.Base qualified
  import MAlonzo.Code.Algebra.Consequences.Setoid qualified
  import MAlonzo.Code.Data.Irrelevant qualified
  import MAlonzo.Code.Data.Sum.Base qualified
  import MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties qualified
  import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
                      mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
                      word64ToNat)
  import MAlonzo.RTE qualified
  
  -- Algebra.Consequences.Propositional._._DistributesOverʳ_
  d__DistributesOver'691'__16 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d__DistributesOver'691'__16 = erased
  -- Algebra.Consequences.Propositional._._DistributesOverˡ_
  d__DistributesOver'737'__18 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d__DistributesOver'737'__18 = erased
  -- Algebra.Consequences.Propositional._._MiddleFourExchange_
  d__MiddleFourExchange__22 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d__MiddleFourExchange__22 = erased
  -- Algebra.Consequences.Propositional._.Associative
  d_Associative_34 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d_Associative_34 = erased
  -- Algebra.Consequences.Propositional._.Commutative
  d_Commutative_38 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d_Commutative_38 = erased
  -- Algebra.Consequences.Propositional._.Idempotent
  d_Idempotent_48 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d_Idempotent_48 = erased
  -- Algebra.Consequences.Propositional._.Identity
  d_Identity_54 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d_Identity_54 = erased
  -- Algebra.Consequences.Propositional._.LeftInverse
  d_LeftInverse_82 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    AgdaAny ->
    (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d_LeftInverse_82 = erased
  -- Algebra.Consequences.Propositional._.LeftZero
  d_LeftZero_88 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d_LeftZero_88 = erased
  -- Algebra.Consequences.Propositional._.RightIdentity
  d_RightIdentity_110 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d_RightIdentity_110 = erased
  -- Algebra.Consequences.Propositional._.RightInverse
  d_RightInverse_112 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    AgdaAny ->
    (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d_RightInverse_112 = erased
  -- Algebra.Consequences.Propositional._.RightZero
  d_RightZero_118 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d_RightZero_118 = erased
  -- Algebra.Consequences.Propositional._.Selective
  d_Selective_120 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> (AgdaAny -> AgdaAny -> AgdaAny) -> ()
  d_Selective_120 = erased
  -- Algebra.Consequences.Propositional.Base.comm+almostCancelʳ⇒almostCancelˡ
  d_comm'43'almostCancel'691''8658'almostCancel'737'_158 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
      MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'43'almostCancel'691''8658'almostCancel'737'_158 = erased
  -- Algebra.Consequences.Propositional.Base.comm+almostCancelˡ⇒almostCancelʳ
  d_comm'43'almostCancel'737''8658'almostCancel'691'_160 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
      MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'43'almostCancel'737''8658'almostCancel'691'_160 = erased
  -- Algebra.Consequences.Propositional.Base.comm+cancelʳ⇒cancelˡ
  d_comm'43'cancel'691''8658'cancel'737'_164 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'43'cancel'691''8658'cancel'737'_164 = erased
  -- Algebra.Consequences.Propositional.Base.comm+cancelˡ⇒cancelʳ
  d_comm'43'cancel'737''8658'cancel'691'_166 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'43'cancel'737''8658'cancel'691'_166 = erased
  -- Algebra.Consequences.Propositional.Base.comm+idʳ⇒idˡ
  d_comm'43'id'691''8658'id'737'_172 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'43'id'691''8658'id'737'_172 = erased
  -- Algebra.Consequences.Propositional.Base.comm+idˡ⇒idʳ
  d_comm'43'id'737''8658'id'691'_174 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'43'id'737''8658'id'691'_174 = erased
  -- Algebra.Consequences.Propositional.Base.comm+invʳ⇒inv
  d_comm'43'inv'691''8658'inv_176 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_comm'43'inv'691''8658'inv_176 ~v0 ~v1
    = du_comm'43'inv'691''8658'inv_176
  du_comm'43'inv'691''8658'inv_176 ::
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_comm'43'inv'691''8658'inv_176
    = coe
        MAlonzo.Code.Algebra.Consequences.Setoid.du_comm'43'inv'691''8658'inv_682
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
  -- Algebra.Consequences.Propositional.Base.comm+invʳ⇒invˡ
  d_comm'43'inv'691''8658'inv'737'_178 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'43'inv'691''8658'inv'737'_178 = erased
  -- Algebra.Consequences.Propositional.Base.comm+invˡ⇒inv
  d_comm'43'inv'737''8658'inv_180 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_comm'43'inv'737''8658'inv_180 ~v0 ~v1
    = du_comm'43'inv'737''8658'inv_180
  du_comm'43'inv'737''8658'inv_180 ::
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_comm'43'inv'737''8658'inv_180
    = coe
        MAlonzo.Code.Algebra.Consequences.Setoid.du_comm'43'inv'737''8658'inv_680
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
  -- Algebra.Consequences.Propositional.Base.comm+invˡ⇒invʳ
  d_comm'43'inv'737''8658'inv'691'_182 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'43'inv'737''8658'inv'691'_182 = erased
  -- Algebra.Consequences.Propositional.Base.comm+zeʳ⇒zeˡ
  d_comm'43'ze'691''8658'ze'737'_184 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'43'ze'691''8658'ze'737'_184 = erased
  -- Algebra.Consequences.Propositional.Base.comm+zeˡ⇒zeʳ
  d_comm'43'ze'737''8658'ze'691'_186 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'43'ze'737''8658'ze'691'_186 = erased
  -- Algebra.Consequences.Propositional.Base.comm∧almostCancelʳ⇒almostCancelˡ
  d_comm'8743'almostCancel'691''8658'almostCancel'737'_190 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
      MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'8743'almostCancel'691''8658'almostCancel'737'_190 = erased
  -- Algebra.Consequences.Propositional.Base.comm∧almostCancelˡ⇒almostCancelʳ
  d_comm'8743'almostCancel'737''8658'almostCancel'691'_192 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
      MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'8743'almostCancel'737''8658'almostCancel'691'_192 = erased
  -- Algebra.Consequences.Propositional.Base.comm∧cancelʳ⇒cancelˡ
  d_comm'8743'cancel'691''8658'cancel'737'_196 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'8743'cancel'691''8658'cancel'737'_196 = erased
  -- Algebra.Consequences.Propositional.Base.comm∧cancelˡ⇒cancelʳ
  d_comm'8743'cancel'737''8658'cancel'691'_198 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'8743'cancel'737''8658'cancel'691'_198 = erased
  -- Algebra.Consequences.Propositional.Base.comm∧distrʳ⇒distr
  d_comm'8743'distr'691''8658'distr_200 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_comm'8743'distr'691''8658'distr_200 ~v0 ~v1
    = du_comm'8743'distr'691''8658'distr_200
  du_comm'8743'distr'691''8658'distr_200 ::
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_comm'8743'distr'691''8658'distr_200
    = coe
        MAlonzo.Code.Algebra.Consequences.Setoid.du_comm'8743'distr'691''8658'distr_528
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
  -- Algebra.Consequences.Propositional.Base.comm∧distrˡ⇒distr
  d_comm'8743'distr'737''8658'distr_204 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_comm'8743'distr'737''8658'distr_204 ~v0 ~v1
    = du_comm'8743'distr'737''8658'distr_204
  du_comm'8743'distr'737''8658'distr_204 ::
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_comm'8743'distr'737''8658'distr_204
    = coe
        MAlonzo.Code.Algebra.Consequences.Setoid.du_comm'8743'distr'737''8658'distr_524
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
  -- Algebra.Consequences.Propositional.Base.comm∧idʳ⇒id
  d_comm'8743'id'691''8658'id_208 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_comm'8743'id'691''8658'id_208 ~v0 ~v1
    = du_comm'8743'id'691''8658'id_208
  du_comm'8743'id'691''8658'id_208 ::
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_comm'8743'id'691''8658'id_208
    = coe
        MAlonzo.Code.Algebra.Consequences.Setoid.du_comm'8743'id'691''8658'id_356
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
  -- Algebra.Consequences.Propositional.Base.comm∧idʳ⇒idˡ
  d_comm'8743'id'691''8658'id'737'_210 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'8743'id'691''8658'id'737'_210 = erased
  -- Algebra.Consequences.Propositional.Base.comm∧idˡ⇒id
  d_comm'8743'id'737''8658'id_212 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_comm'8743'id'737''8658'id_212 ~v0 ~v1
    = du_comm'8743'id'737''8658'id_212
  du_comm'8743'id'737''8658'id_212 ::
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_comm'8743'id'737''8658'id_212
    = coe
        MAlonzo.Code.Algebra.Consequences.Setoid.du_comm'8743'id'737''8658'id_352
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
  -- Algebra.Consequences.Propositional.Base.comm∧idˡ⇒idʳ
  d_comm'8743'id'737''8658'id'691'_214 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'8743'id'737''8658'id'691'_214 = erased
  -- Algebra.Consequences.Propositional.Base.comm∧invʳ⇒inv
  d_comm'8743'inv'691''8658'inv_216 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_comm'8743'inv'691''8658'inv_216 ~v0 ~v1
    = du_comm'8743'inv'691''8658'inv_216
  du_comm'8743'inv'691''8658'inv_216 ::
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_comm'8743'inv'691''8658'inv_216
    = coe
        MAlonzo.Code.Algebra.Consequences.Setoid.du_comm'8743'inv'691''8658'inv_436
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
  -- Algebra.Consequences.Propositional.Base.comm∧invʳ⇒invˡ
  d_comm'8743'inv'691''8658'inv'737'_218 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'8743'inv'691''8658'inv'737'_218 = erased
  -- Algebra.Consequences.Propositional.Base.comm∧invˡ⇒inv
  d_comm'8743'inv'737''8658'inv_220 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_comm'8743'inv'737''8658'inv_220 ~v0 ~v1
    = du_comm'8743'inv'737''8658'inv_220
  du_comm'8743'inv'737''8658'inv_220 ::
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_comm'8743'inv'737''8658'inv_220
    = coe
        MAlonzo.Code.Algebra.Consequences.Setoid.du_comm'8743'inv'737''8658'inv_426
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
  -- Algebra.Consequences.Propositional.Base.comm∧invˡ⇒invʳ
  d_comm'8743'inv'737''8658'inv'691'_222 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'8743'inv'737''8658'inv'691'_222 = erased
  -- Algebra.Consequences.Propositional.Base.comm∧zeʳ⇒ze
  d_comm'8743'ze'691''8658'ze_224 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_comm'8743'ze'691''8658'ze_224 ~v0 ~v1
    = du_comm'8743'ze'691''8658'ze_224
  du_comm'8743'ze'691''8658'ze_224 ::
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_comm'8743'ze'691''8658'ze_224
    = coe
        MAlonzo.Code.Algebra.Consequences.Setoid.du_comm'8743'ze'691''8658'ze_376
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
  -- Algebra.Consequences.Propositional.Base.comm∧zeʳ⇒zeˡ
  d_comm'8743'ze'691''8658'ze'737'_226 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'8743'ze'691''8658'ze'737'_226 = erased
  -- Algebra.Consequences.Propositional.Base.comm∧zeˡ⇒ze
  d_comm'8743'ze'737''8658'ze_228 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_comm'8743'ze'737''8658'ze_228 ~v0 ~v1
    = du_comm'8743'ze'737''8658'ze_228
  du_comm'8743'ze'737''8658'ze_228 ::
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_comm'8743'ze'737''8658'ze_228
    = coe
        MAlonzo.Code.Algebra.Consequences.Setoid.du_comm'8743'ze'737''8658'ze_372
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
  -- Algebra.Consequences.Propositional.Base.comm∧zeˡ⇒zeʳ
  d_comm'8743'ze'737''8658'ze'691'_230 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'8743'ze'737''8658'ze'691'_230 = erased
  -- Algebra.Consequences.Propositional.Base.distrib∧absorbs⇒distribˡ
  d_distrib'8743'absorbs'8658'distrib'737'_232 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_distrib'8743'absorbs'8658'distrib'737'_232 = erased
  -- Algebra.Consequences.Propositional.Base.selfInverse⇒bijective
  d_selfInverse'8658'bijective_242 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_selfInverse'8658'bijective_242 ~v0 ~v1
    = du_selfInverse'8658'bijective_242
  du_selfInverse'8658'bijective_242 ::
    (AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_selfInverse'8658'bijective_242
    = coe
        MAlonzo.Code.Algebra.Consequences.Setoid.du_selfInverse'8658'bijective_296
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
  -- Algebra.Consequences.Propositional.Base.selfInverse⇒congruent
  d_selfInverse'8658'congruent_244 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_selfInverse'8658'congruent_244 = erased
  -- Algebra.Consequences.Propositional.Base.selfInverse⇒injective
  d_selfInverse'8658'injective_246 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_selfInverse'8658'injective_246 = erased
  -- Algebra.Consequences.Propositional.Base.selfInverse⇒inverseᵇ
  d_selfInverse'8658'inverse'7495'_248 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_selfInverse'8658'inverse'7495'_248 ~v0 ~v1
    = du_selfInverse'8658'inverse'7495'_248
  du_selfInverse'8658'inverse'7495'_248 ::
    (AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_selfInverse'8658'inverse'7495'_248
    = coe
        MAlonzo.Code.Algebra.Consequences.Setoid.du_selfInverse'8658'inverse'7495'_282
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
  -- Algebra.Consequences.Propositional.Base.selfInverse⇒involutive
  d_selfInverse'8658'involutive_250 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_selfInverse'8658'involutive_250 = erased
  -- Algebra.Consequences.Propositional.Base.selfInverse⇒surjective
  d_selfInverse'8658'surjective_252 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_selfInverse'8658'surjective_252 ~v0 ~v1
    = du_selfInverse'8658'surjective_252
  du_selfInverse'8658'surjective_252 ::
    (AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_selfInverse'8658'surjective_252
    = coe
        MAlonzo.Code.Algebra.Consequences.Setoid.du_selfInverse'8658'surjective_284
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
  -- Algebra.Consequences.Propositional.Base.Base.reflexive+selfInverse⇒involutive
  d_reflexive'43'selfInverse'8658'involutive_262 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
  d_reflexive'43'selfInverse'8658'involutive_262 ~v0 ~v1
    = du_reflexive'43'selfInverse'8658'involutive_262
  du_reflexive'43'selfInverse'8658'involutive_262 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
  du_reflexive'43'selfInverse'8658'involutive_262 v0 v1
    = coe
        MAlonzo.Code.Algebra.Consequences.Base.du_reflexive'43'selfInverse'8658'involutive_42
  -- Algebra.Consequences.Propositional.Base._.reflexive∧selfInverse⇒involutive
  d_reflexive'8743'selfInverse'8658'involutive_266 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
  d_reflexive'8743'selfInverse'8658'involutive_266 ~v0 ~v1
    = du_reflexive'8743'selfInverse'8658'involutive_266
  du_reflexive'8743'selfInverse'8658'involutive_266 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
  du_reflexive'8743'selfInverse'8658'involutive_266 v0 v1 v2 v3 v4 v5
                                                    v6 v7
    = coe
        MAlonzo.Code.Algebra.Consequences.Base.du_reflexive'8743'selfInverse'8658'involutive_36
        v3 v5 v6 v7
  -- Algebra.Consequences.Propositional._.assoc∧id∧invʳ⇒invˡ-unique
  d_assoc'8743'id'8743'inv'691''8658'inv'737''45'unique_286 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_assoc'8743'id'8743'inv'691''8658'inv'737''45'unique_286 = erased
  -- Algebra.Consequences.Propositional._.assoc∧id∧invˡ⇒invʳ-unique
  d_assoc'8743'id'8743'inv'737''8658'inv'691''45'unique_292 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_assoc'8743'id'8743'inv'737''8658'inv'691''45'unique_292 = erased
  -- Algebra.Consequences.Propositional._.assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ
  d_assoc'8743'distrib'691''8743'id'691''8743'inv'691''8658'ze'737'_306 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_assoc'8743'distrib'691''8743'id'691''8743'inv'691''8658'ze'737'_306
    = erased
  -- Algebra.Consequences.Propositional._.assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ
  d_assoc'8743'distrib'737''8743'id'691''8743'inv'691''8658'ze'691'_308 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_assoc'8743'distrib'737''8743'id'691''8743'inv'691''8658'ze'691'_308
    = erased
  -- Algebra.Consequences.Propositional._.comm∧distrˡ⇒distrʳ
  d_comm'8743'distr'737''8658'distr'691'_320 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'8743'distr'737''8658'distr'691'_320 = erased
  -- Algebra.Consequences.Propositional._.comm∧distrʳ⇒distrˡ
  d_comm'8743'distr'691''8658'distr'737'_322 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'8743'distr'691''8658'distr'737'_322 = erased
  -- Algebra.Consequences.Propositional._.comm⇒sym[distribˡ]
  d_comm'8658'sym'91'distrib'737''93'_330 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'8658'sym'91'distrib'737''93'_330 = erased
  -- Algebra.Consequences.Propositional._.sel⇒idem
  d_sel'8658'idem_338 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_sel'8658'idem_338 = erased
  -- Algebra.Consequences.Propositional._.comm∧assoc⇒middleFour
  d_comm'8743'assoc'8658'middleFour_346 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'8743'assoc'8658'middleFour_346 = erased
  -- Algebra.Consequences.Propositional._.identity∧middleFour⇒assoc
  d_identity'8743'middleFour'8658'assoc_350 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_identity'8743'middleFour'8658'assoc_350 = erased
  -- Algebra.Consequences.Propositional._.identity∧middleFour⇒comm
  d_identity'8743'middleFour'8658'comm_356 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_identity'8743'middleFour'8658'comm_356 = erased
  -- Algebra.Consequences.Propositional._.subst∧comm⇒sym
  d_subst'8743'comm'8658'sym_374 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_subst'8743'comm'8658'sym_374 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8
    = du_subst'8743'comm'8658'sym_374 v8
  du_subst'8743'comm'8658'sym_374 :: AgdaAny -> AgdaAny
  du_subst'8743'comm'8658'sym_374 v0 = coe v0
  -- Algebra.Consequences.Propositional._.wlog
  d_wlog_392 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny
  d_wlog_392 ~v0 ~v1 ~v2 ~v3 v4 = du_wlog_392 v4
  du_wlog_392 ::
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> AgdaAny
  du_wlog_392 v0 v1 v2 v3 v4
    = coe
        MAlonzo.Code.Algebra.Consequences.Setoid.du_wlog_650 (coe v0)
        erased (coe (\ v5 v6 v7 v8 v9 -> v9)) v1 v4
  -- Algebra.Consequences.Propositional.comm+assoc⇒middleFour
  d_comm'43'assoc'8658'middleFour_394 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'43'assoc'8658'middleFour_394 = erased
  -- Algebra.Consequences.Propositional.identity+middleFour⇒assoc
  d_identity'43'middleFour'8658'assoc_396 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_identity'43'middleFour'8658'assoc_396 = erased
  -- Algebra.Consequences.Propositional.identity+middleFour⇒comm
  d_identity'43'middleFour'8658'comm_398 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_identity'43'middleFour'8658'comm_398 = erased
  -- Algebra.Consequences.Propositional.comm+distrˡ⇒distrʳ
  d_comm'43'distr'737''8658'distr'691'_400 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'43'distr'737''8658'distr'691'_400 = erased
  -- Algebra.Consequences.Propositional.comm+distrʳ⇒distrˡ
  d_comm'43'distr'691''8658'distr'737'_402 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_comm'43'distr'691''8658'distr'737'_402 = erased
  -- Algebra.Consequences.Propositional.assoc+distribʳ+idʳ+invʳ⇒zeˡ
  d_assoc'43'distrib'691''43'id'691''43'inv'691''8658'ze'737'_404 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_assoc'43'distrib'691''43'id'691''43'inv'691''8658'ze'737'_404
    = erased
  -- Algebra.Consequences.Propositional.assoc+distribˡ+idʳ+invʳ⇒zeʳ
  d_assoc'43'distrib'737''43'id'691''43'inv'691''8658'ze'691'_406 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_assoc'43'distrib'737''43'id'691''43'inv'691''8658'ze'691'_406
    = erased
  -- Algebra.Consequences.Propositional.assoc+id+invʳ⇒invˡ-unique
  d_assoc'43'id'43'inv'691''8658'inv'737''45'unique_408 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_assoc'43'id'43'inv'691''8658'inv'737''45'unique_408 = erased
  -- Algebra.Consequences.Propositional.assoc+id+invˡ⇒invʳ-unique
  d_assoc'43'id'43'inv'737''8658'inv'691''45'unique_410 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_assoc'43'id'43'inv'737''8658'inv'691''45'unique_410 = erased
  -- Algebra.Consequences.Propositional.subst+comm⇒sym
  d_subst'43'comm'8658'sym_412 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
  d_subst'43'comm'8658'sym_412 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8
    = du_subst'43'comm'8658'sym_412 v8
  du_subst'43'comm'8658'sym_412 :: AgdaAny -> AgdaAny
  du_subst'43'comm'8658'sym_412 v0 = coe v0
  