{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Relation.Binary.PropositionalEquality.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.Equality
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Properties.Setoid
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core

-- Relation.Binary.PropositionalEquality.Properties.J
d_J_34 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  (AgdaAny ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> ()) ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  AgdaAny -> AgdaAny
d_J_34 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> (AgdaAny -> T__'8801'__12 -> T_Level_18)
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
d_J_34 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny
v3 ~AgdaAny -> T__'8801'__12 -> T_Level_18
v4 ~AgdaAny
v5 ~T__'8801'__12
v6 AgdaAny
v7 = AgdaAny -> AgdaAny
du_J_34 AgdaAny
v7
du_J_34 :: AgdaAny -> AgdaAny
du_J_34 :: AgdaAny -> AgdaAny
du_J_34 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Relation.Binary.PropositionalEquality.Properties.dcong
d_dcong_54 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_dcong_54 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_dcong_54 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties.dcong₂
d_dcong'8322'_78 ::
  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 ->
  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_dcong'8322'_78 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
d_dcong'8322'_78 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties.dsubst₂
d_dsubst'8322'_100 ::
  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 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  AgdaAny -> AgdaAny
d_dsubst'8322'_100 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
d_dsubst'8322'_100 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 ~AgdaAny
v6 ~AgdaAny
v7 ~AgdaAny
v8 ~AgdaAny
v9 ~T__'8801'__12
v10
                   ~T__'8801'__12
v11 AgdaAny
v12
  = AgdaAny -> AgdaAny
du_dsubst'8322'_100 AgdaAny
v12
du_dsubst'8322'_100 :: AgdaAny -> AgdaAny
du_dsubst'8322'_100 :: AgdaAny -> AgdaAny
du_dsubst'8322'_100 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Relation.Binary.PropositionalEquality.Properties.ddcong₂
d_ddcong'8322'_132 ::
  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 ->
  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_ddcong'8322'_132 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
d_ddcong'8322'_132 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties.trans-reflʳ
d_trans'45'refl'691'_142 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_trans'45'refl'691'_142 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_trans'45'refl'691'_142 = T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties.trans-assoc
d_trans'45'assoc_158 ::
  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.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_trans'45'assoc_158 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
d_trans'45'assoc_158 = T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties.trans-symˡ
d_trans'45'sym'737'_166 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_trans'45'sym'737'_166 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_trans'45'sym'737'_166 = T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties.trans-symʳ
d_trans'45'sym'691'_174 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_trans'45'sym'691'_174 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_trans'45'sym'691'_174 = T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties.trans-injectiveˡ
d_trans'45'injective'737'_188 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  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 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_trans'45'injective'737'_188 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
d_trans'45'injective'737'_188 = T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties.trans-injectiveʳ
d_trans'45'injective'691'_202 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  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 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_trans'45'injective'691'_202 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
d_trans'45'injective'691'_202 = T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties.cong-id
d_cong'45'id_212 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_cong'45'id_212 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_cong'45'id_212 = T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties.cong-∘
d_cong'45''8728'_224 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_cong'45''8728'_224 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T__'8801'__12
-> T__'8801'__12
d_cong'45''8728'_224 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties.sym-cong
d_sym'45'cong_234 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  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
d_sym'45'cong_234 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T__'8801'__12
-> T__'8801'__12
d_sym'45'cong_234 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties.trans-cong
d_trans'45'cong_248 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_trans'45'cong_248 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
d_trans'45'cong_248 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties.cong₂-reflˡ
d_cong'8322''45'refl'737'_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 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_cong'8322''45'refl'737'_262 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_cong'8322''45'refl'737'_262 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties.cong₂-reflʳ
d_cong'8322''45'refl'691'_276 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_cong'8322''45'refl'691'_276 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_cong'8322''45'refl'691'_276 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties._.subst-injective
d_subst'45'injective_298 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (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.Equality.T__'8801'__12
d_subst'45'injective_298 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_subst'45'injective_298 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties._.subst-subst
d_subst'45'subst_310 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  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_subst'45'subst_310 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
d_subst'45'subst_310 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties._.subst-subst-sym
d_subst'45'subst'45'sym_316 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subst'45'subst'45'sym_316 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
d_subst'45'subst'45'sym_316 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties._.subst-sym-subst
d_subst'45'sym'45'subst_322 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subst'45'sym'45'subst_322 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
d_subst'45'sym'45'subst_322 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties.subst-∘
d_subst'45''8728'_336 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subst'45''8728'_336 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
d_subst'45''8728'_336 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties.subst-application′
d_subst'45'application'8242'_362 ::
  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) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subst'45'application'8242'_362 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
-> T__'8801'__12
d_subst'45'application'8242'_362 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties.subst-application
d_subst'45'application_394 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  (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
d_subst'45'application_394 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
-> T__'8801'__12
d_subst'45'application_394 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties.isEquivalence
d_isEquivalence_396 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_isEquivalence_396 :: T_Level_18 -> T_Level_18 -> T_IsEquivalence_26
d_isEquivalence_396 ~T_Level_18
v0 ~T_Level_18
v1 = T_IsEquivalence_26
du_isEquivalence_396
du_isEquivalence_396 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
du_isEquivalence_396 :: T_IsEquivalence_26
du_isEquivalence_396
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_745
      AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties.isDecEquivalence
d_isDecEquivalence_398 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
d_isDecEquivalence_398 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsDecEquivalence_44
d_isDecEquivalence_398 ~T_Level_18
v0 ~T_Level_18
v1 AgdaAny -> AgdaAny -> T_Dec_20
v2 = (AgdaAny -> AgdaAny -> T_Dec_20) -> T_IsDecEquivalence_44
du_isDecEquivalence_398 AgdaAny -> AgdaAny -> T_Dec_20
v2
du_isDecEquivalence_398 ::
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
du_isDecEquivalence_398 :: (AgdaAny -> AgdaAny -> T_Dec_20) -> T_IsDecEquivalence_44
du_isDecEquivalence_398 AgdaAny -> AgdaAny -> T_Dec_20
v0
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> T_Dec_20) -> T_IsDecEquivalence_44)
-> AgdaAny -> AgdaAny -> T_IsDecEquivalence_44
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> T_Dec_20) -> T_IsDecEquivalence_44
MAlonzo.Code.Relation.Binary.Structures.C_IsDecEquivalence'46'constructor_3083
      (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
du_isEquivalence_396) ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v0)
-- Relation.Binary.PropositionalEquality.Properties.setoid
d_setoid_402 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_setoid_402 :: T_Level_18 -> T_Level_18 -> T_Setoid_44
d_setoid_402 ~T_Level_18
v0 ~T_Level_18
v1 = T_Setoid_44
du_setoid_402
du_setoid_402 :: MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du_setoid_402 :: T_Setoid_44
du_setoid_402
  = (T_IsEquivalence_26 -> T_Setoid_44) -> AgdaAny -> T_Setoid_44
forall a b. a -> b
coe
      T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_733
      (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
du_isEquivalence_396)
-- Relation.Binary.PropositionalEquality.Properties.decSetoid
d_decSetoid_406 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
d_decSetoid_406 :: T_Level_18
-> T_Level_18 -> (AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecSetoid_84
d_decSetoid_406 ~T_Level_18
v0 ~T_Level_18
v1 AgdaAny -> AgdaAny -> T_Dec_20
v2 = (AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecSetoid_84
du_decSetoid_406 AgdaAny -> AgdaAny -> T_Dec_20
v2
du_decSetoid_406 ::
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
du_decSetoid_406 :: (AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecSetoid_84
du_decSetoid_406 AgdaAny -> AgdaAny -> T_Dec_20
v0
  = (T_IsDecEquivalence_44 -> T_DecSetoid_84)
-> AgdaAny -> T_DecSetoid_84
forall a b. a -> b
coe
      T_IsDecEquivalence_44 -> T_DecSetoid_84
MAlonzo.Code.Relation.Binary.Bundles.C_DecSetoid'46'constructor_1389
      (((AgdaAny -> AgdaAny -> T_Dec_20) -> T_IsDecEquivalence_44)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Dec_20) -> T_IsDecEquivalence_44
du_isDecEquivalence_398 ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v0))
-- Relation.Binary.PropositionalEquality.Properties.isPreorder
d_isPreorder_410 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_isPreorder_410 :: T_Level_18 -> T_Level_18 -> T_IsPreorder_70
d_isPreorder_410 ~T_Level_18
v0 ~T_Level_18
v1 = T_IsPreorder_70
du_isPreorder_410
du_isPreorder_410 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
du_isPreorder_410 :: T_IsPreorder_70
du_isPreorder_410
  = (T_Setoid_44 -> T_IsPreorder_70) -> AgdaAny -> T_IsPreorder_70
forall a b. a -> b
coe
      T_Setoid_44 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Properties.Setoid.du_'8776''45'isPreorder_38
      (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
du_setoid_402)
-- Relation.Binary.PropositionalEquality.Properties.isPartialOrder
d_isPartialOrder_412 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
d_isPartialOrder_412 :: T_Level_18 -> T_Level_18 -> T_IsPartialOrder_174
d_isPartialOrder_412 ~T_Level_18
v0 ~T_Level_18
v1 = T_IsPartialOrder_174
du_isPartialOrder_412
du_isPartialOrder_412 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
du_isPartialOrder_412 :: T_IsPartialOrder_174
du_isPartialOrder_412
  = (T_Setoid_44 -> T_IsPartialOrder_174)
-> AgdaAny -> T_IsPartialOrder_174
forall a b. a -> b
coe
      T_Setoid_44 -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Properties.Setoid.du_'8776''45'isPartialOrder_40
      (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
du_setoid_402)
-- Relation.Binary.PropositionalEquality.Properties.preorder
d_preorder_414 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_preorder_414 :: T_Level_18 -> T_Level_18 -> T_Preorder_132
d_preorder_414 ~T_Level_18
v0 ~T_Level_18
v1 = T_Preorder_132
du_preorder_414
du_preorder_414 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_preorder_414 :: T_Preorder_132
du_preorder_414
  = (T_Setoid_44 -> T_Preorder_132) -> AgdaAny -> T_Preorder_132
forall a b. a -> b
coe
      T_Setoid_44 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Properties.Setoid.du_'8776''45'preorder_48
      (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
du_setoid_402)
-- Relation.Binary.PropositionalEquality.Properties.poset
d_poset_418 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314
d_poset_418 :: T_Level_18 -> T_Level_18 -> T_Poset_314
d_poset_418 ~T_Level_18
v0 ~T_Level_18
v1 = T_Poset_314
du_poset_418
du_poset_418 :: MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314
du_poset_418 :: T_Poset_314
du_poset_418
  = (T_Setoid_44 -> T_Poset_314) -> AgdaAny -> T_Poset_314
forall a b. a -> b
coe
      T_Setoid_44 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Properties.Setoid.du_'8776''45'poset_50
      (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe T_Setoid_44
du_setoid_402)
-- Relation.Binary.PropositionalEquality.Properties.≡-Reasoning._.begin_
d_begin__430 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_begin__430 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_begin__430 = T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties.≡-Reasoning._.step-≡
d_step'45''8801'_434 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  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
d_step'45''8801'_434 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
d_step'45''8801'_434 = T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties.≡-Reasoning._.step-≡-∣
d_step'45''8801''45''8739'_436 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_step'45''8801''45''8739'_436 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_step'45''8801''45''8739'_436 = T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties.≡-Reasoning._.step-≡-⟨
d_step'45''8801''45''10216'_438 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  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
d_step'45''8801''45''10216'_438 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
d_step'45''8801''45''10216'_438 = T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties.≡-Reasoning._.step-≡-⟩
d_step'45''8801''45''10217'_440 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  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
d_step'45''8801''45''10217'_440 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
d_step'45''8801''45''10217'_440 = T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties.≡-Reasoning._.step-≡˘
d_step'45''8801''728'_442 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  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
d_step'45''8801''728'_442 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
d_step'45''8801''728'_442 = T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Relation.Binary.PropositionalEquality.Properties.≡-Reasoning._._∎
d__'8718'_446 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d__'8718'_446 :: T_Level_18 -> T_Level_18 -> AgdaAny -> T__'8801'__12
d__'8718'_446 = T_Level_18 -> T_Level_18 -> AgdaAny -> T__'8801'__12
forall a. a
erased