{-# 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.Untyped.RenamingSubstitution 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.Builtin.List
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Untyped

-- Untyped.RenamingSubstitution.Ren
d_Ren_4 :: () -> () -> ()
d_Ren_4 :: () -> () -> ()
d_Ren_4 = () -> () -> ()
forall a. a
erased
-- Untyped.RenamingSubstitution.lift
d_lift_14 ::
  () -> () -> (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
d_lift_14 :: () -> () -> (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
d_lift_14 ~()
v0 ~()
v1 AgdaAny -> AgdaAny
v2 Maybe AgdaAny
v3 = (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
du_lift_14 AgdaAny -> AgdaAny
v2 Maybe AgdaAny
v3
du_lift_14 ::
  (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
du_lift_14 :: (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
du_lift_14 AgdaAny -> AgdaAny
v0 Maybe AgdaAny
v1
  = case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
      MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v2
        -> (AgdaAny -> Maybe AgdaAny) -> AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v2)
      Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1
      Maybe AgdaAny
_ -> Maybe AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.RenamingSubstitution.renList
d_renList_26 ::
  () ->
  () ->
  (AgdaAny -> AgdaAny) ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  [MAlonzo.Code.Untyped.T__'8866'_14]
d_renList_26 :: ()
-> () -> (AgdaAny -> AgdaAny) -> [T__'8866'_14] -> [T__'8866'_14]
d_renList_26 ~()
v0 ~()
v1 AgdaAny -> AgdaAny
v2 [T__'8866'_14]
v3 = (AgdaAny -> AgdaAny) -> [T__'8866'_14] -> [T__'8866'_14]
du_renList_26 AgdaAny -> AgdaAny
v2 [T__'8866'_14]
v3
du_renList_26 ::
  (AgdaAny -> AgdaAny) ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  [MAlonzo.Code.Untyped.T__'8866'_14]
du_renList_26 :: (AgdaAny -> AgdaAny) -> [T__'8866'_14] -> [T__'8866'_14]
du_renList_26 AgdaAny -> AgdaAny
v0 [T__'8866'_14]
v1
  = case [T__'8866'_14] -> [AgdaAny]
forall a b. a -> b
coe [T__'8866'_14]
v1 of
      [] -> [T__'8866'_14] -> [T__'8866'_14]
forall a b. a -> b
coe [T__'8866'_14]
v1
      (:) AgdaAny
v2 [AgdaAny]
v3
        -> (AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> [T__'8866'_14]
forall a b. a -> b
coe
             AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
             (((AgdaAny -> AgdaAny) -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> T__'8866'_14 -> T__'8866'_14
du_ren_32 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
             (((AgdaAny -> AgdaAny) -> [T__'8866'_14] -> [T__'8866'_14])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> [T__'8866'_14] -> [T__'8866'_14]
du_renList_26 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3))
      [AgdaAny]
_ -> [T__'8866'_14]
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.RenamingSubstitution.ren
d_ren_32 ::
  () ->
  () ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14
d_ren_32 :: () -> () -> (AgdaAny -> AgdaAny) -> T__'8866'_14 -> T__'8866'_14
d_ren_32 ~()
v0 ~()
v1 AgdaAny -> AgdaAny
v2 T__'8866'_14
v3 = (AgdaAny -> AgdaAny) -> T__'8866'_14 -> T__'8866'_14
du_ren_32 AgdaAny -> AgdaAny
v2 T__'8866'_14
v3
du_ren_32 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14
du_ren_32 :: (AgdaAny -> AgdaAny) -> T__'8866'_14 -> T__'8866'_14
du_ren_32 AgdaAny -> AgdaAny
v0 T__'8866'_14
v1
  = case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
      MAlonzo.Code.Untyped.C_'96'_18 AgdaAny
v2
        -> (AgdaAny -> T__'8866'_14) -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe AgdaAny -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v2)
      MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v2
        -> (T__'8866'_14 -> T__'8866'_14) -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
             T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
             (((AgdaAny -> AgdaAny) -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> T__'8866'_14 -> T__'8866'_14
du_ren_32 (((AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
du_lift_14 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0)) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2))
      MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v2 T__'8866'_14
v3
        -> (T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
             T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22 (((AgdaAny -> AgdaAny) -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> T__'8866'_14 -> T__'8866'_14
du_ren_32 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2))
             (((AgdaAny -> AgdaAny) -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> T__'8866'_14 -> T__'8866'_14
du_ren_32 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v3))
      MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v2
        -> (T__'8866'_14 -> T__'8866'_14) -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
             T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_force_24 (((AgdaAny -> AgdaAny) -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> T__'8866'_14 -> T__'8866'_14
du_ren_32 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2))
      MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v2
        -> (T__'8866'_14 -> T__'8866'_14) -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
             T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_delay_26 (((AgdaAny -> AgdaAny) -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> T__'8866'_14 -> T__'8866'_14
du_ren_32 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2))
      MAlonzo.Code.Untyped.C_con_28 T_TmCon_198
v2 -> T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1
      MAlonzo.Code.Untyped.C_constr_34 Integer
v2 [T__'8866'_14]
v3
        -> (Integer -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
             Integer -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_constr_34 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2)
             (((AgdaAny -> AgdaAny) -> [T__'8866'_14] -> [T__'8866'_14])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> [T__'8866'_14] -> [T__'8866'_14]
du_renList_26 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) ([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v3))
      MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v2 [T__'8866'_14]
v3
        -> (T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
             T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40 (((AgdaAny -> AgdaAny) -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> T__'8866'_14 -> T__'8866'_14
du_ren_32 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2))
             (((AgdaAny -> AgdaAny) -> [T__'8866'_14] -> [T__'8866'_14])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> [T__'8866'_14] -> [T__'8866'_14]
du_renList_26 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) ([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v3))
      MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v2 -> T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1
      T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 -> T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1
      T__'8866'_14
_ -> T__'8866'_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.RenamingSubstitution.weaken
d_weaken_88 ::
  () ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14
d_weaken_88 :: () -> T__'8866'_14 -> T__'8866'_14
d_weaken_88 ~()
v0 T__'8866'_14
v1 = T__'8866'_14 -> T__'8866'_14
du_weaken_88 T__'8866'_14
v1
du_weaken_88 ::
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14
du_weaken_88 :: T__'8866'_14 -> T__'8866'_14
du_weaken_88 T__'8866'_14
v0
  = ((AgdaAny -> AgdaAny) -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> T__'8866'_14 -> T__'8866'_14
du_ren_32 ((AgdaAny -> Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v0)
-- Untyped.RenamingSubstitution.lift-cong
d_lift'45'cong_104 ::
  () ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lift'45'cong_104 :: ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> Maybe AgdaAny
-> T__'8801'__12
d_lift'45'cong_104 = ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> Maybe AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Untyped.RenamingSubstitution.renList-cong
d_renList'45'cong_124 ::
  () ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_renList'45'cong_124 :: ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> [T__'8866'_14]
-> T__'8801'__12
d_renList'45'cong_124 = ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> [T__'8866'_14]
-> T__'8801'__12
forall a. a
erased
-- Untyped.RenamingSubstitution.ren-cong
d_ren'45'cong_138 ::
  () ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_ren'45'cong_138 :: ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> T__'8866'_14
-> T__'8801'__12
d_ren'45'cong_138 = ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> T__'8866'_14
-> T__'8801'__12
forall a. a
erased
-- Untyped.RenamingSubstitution.lift-id
d_lift'45'id_196 ::
  () ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lift'45'id_196 :: () -> Maybe AgdaAny -> T__'8801'__12
d_lift'45'id_196 = () -> Maybe AgdaAny -> T__'8801'__12
forall a. a
erased
-- Untyped.RenamingSubstitution.lift-comp
d_lift'45'comp_212 ::
  () ->
  () ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lift'45'comp_212 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T__'8801'__12
d_lift'45'comp_212 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Untyped.RenamingSubstitution.renList-id
d_renList'45'id_228 ::
  () ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_renList'45'id_228 :: () -> [T__'8866'_14] -> T__'8801'__12
d_renList'45'id_228 = () -> [T__'8866'_14] -> T__'8801'__12
forall a. a
erased
-- Untyped.RenamingSubstitution.ren-id
d_ren'45'id_234 ::
  () ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_ren'45'id_234 :: () -> T__'8866'_14 -> T__'8801'__12
d_ren'45'id_234 = () -> T__'8866'_14 -> T__'8801'__12
forall a. a
erased
-- Untyped.RenamingSubstitution.renList-comp
d_renList'45'comp_276 ::
  () ->
  () ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_renList'45'comp_276 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> [T__'8866'_14]
-> T__'8801'__12
d_renList'45'comp_276 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> [T__'8866'_14]
-> T__'8801'__12
forall a. a
erased
-- Untyped.RenamingSubstitution.ren-comp
d_ren'45'comp_290 ::
  () ->
  () ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_ren'45'comp_290 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T__'8866'_14
-> T__'8801'__12
d_ren'45'comp_290 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T__'8866'_14
-> T__'8801'__12
forall a. a
erased
-- Untyped.RenamingSubstitution.Sub
d_Sub_368 :: () -> () -> ()
d_Sub_368 :: () -> () -> ()
d_Sub_368 = () -> () -> ()
forall a. a
erased
-- Untyped.RenamingSubstitution.lifts
d_lifts_378 ::
  () ->
  () ->
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  Maybe AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14
d_lifts_378 :: ()
-> () -> (AgdaAny -> T__'8866'_14) -> Maybe AgdaAny -> T__'8866'_14
d_lifts_378 ~()
v0 ~()
v1 AgdaAny -> T__'8866'_14
v2 Maybe AgdaAny
v3 = (AgdaAny -> T__'8866'_14) -> Maybe AgdaAny -> T__'8866'_14
du_lifts_378 AgdaAny -> T__'8866'_14
v2 Maybe AgdaAny
v3
du_lifts_378 ::
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  Maybe AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14
du_lifts_378 :: (AgdaAny -> T__'8866'_14) -> Maybe AgdaAny -> T__'8866'_14
du_lifts_378 AgdaAny -> T__'8866'_14
v0 Maybe AgdaAny
v1
  = case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
      MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v2
        -> ((AgdaAny -> AgdaAny) -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
             (AgdaAny -> AgdaAny) -> T__'8866'_14 -> T__'8866'_14
du_ren_32 ((AgdaAny -> Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16)
             ((AgdaAny -> T__'8866'_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8866'_14
v0 AgdaAny
v2)
      Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
        -> (AgdaAny -> T__'8866'_14) -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe AgdaAny -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18 (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1)
      Maybe AgdaAny
_ -> T__'8866'_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.RenamingSubstitution.subList
d_subList_390 ::
  () ->
  () ->
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  [MAlonzo.Code.Untyped.T__'8866'_14]
d_subList_390 :: ()
-> ()
-> (AgdaAny -> T__'8866'_14)
-> [T__'8866'_14]
-> [T__'8866'_14]
d_subList_390 ~()
v0 ~()
v1 AgdaAny -> T__'8866'_14
v2 [T__'8866'_14]
v3 = (AgdaAny -> T__'8866'_14) -> [T__'8866'_14] -> [T__'8866'_14]
du_subList_390 AgdaAny -> T__'8866'_14
v2 [T__'8866'_14]
v3
du_subList_390 ::
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  [MAlonzo.Code.Untyped.T__'8866'_14]
du_subList_390 :: (AgdaAny -> T__'8866'_14) -> [T__'8866'_14] -> [T__'8866'_14]
du_subList_390 AgdaAny -> T__'8866'_14
v0 [T__'8866'_14]
v1
  = case [T__'8866'_14] -> [AgdaAny]
forall a b. a -> b
coe [T__'8866'_14]
v1 of
      [] -> [T__'8866'_14] -> [T__'8866'_14]
forall a b. a -> b
coe [T__'8866'_14]
v1
      (:) AgdaAny
v2 [AgdaAny]
v3
        -> (AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> [T__'8866'_14]
forall a b. a -> b
coe
             AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
             (((AgdaAny -> T__'8866'_14) -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T__'8866'_14) -> T__'8866'_14 -> T__'8866'_14
du_sub_396 ((AgdaAny -> T__'8866'_14) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8866'_14
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
             (((AgdaAny -> T__'8866'_14) -> [T__'8866'_14] -> [T__'8866'_14])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T__'8866'_14) -> [T__'8866'_14] -> [T__'8866'_14]
du_subList_390 ((AgdaAny -> T__'8866'_14) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8866'_14
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3))
      [AgdaAny]
_ -> [T__'8866'_14]
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.RenamingSubstitution.sub
d_sub_396 ::
  () ->
  () ->
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14
d_sub_396 :: ()
-> () -> (AgdaAny -> T__'8866'_14) -> T__'8866'_14 -> T__'8866'_14
d_sub_396 ~()
v0 ~()
v1 AgdaAny -> T__'8866'_14
v2 T__'8866'_14
v3 = (AgdaAny -> T__'8866'_14) -> T__'8866'_14 -> T__'8866'_14
du_sub_396 AgdaAny -> T__'8866'_14
v2 T__'8866'_14
v3
du_sub_396 ::
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14
du_sub_396 :: (AgdaAny -> T__'8866'_14) -> T__'8866'_14 -> T__'8866'_14
du_sub_396 AgdaAny -> T__'8866'_14
v0 T__'8866'_14
v1
  = case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
      MAlonzo.Code.Untyped.C_'96'_18 AgdaAny
v2 -> (AgdaAny -> T__'8866'_14) -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe AgdaAny -> T__'8866'_14
v0 AgdaAny
v2
      MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v2
        -> (T__'8866'_14 -> T__'8866'_14) -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
             T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
             (((AgdaAny -> T__'8866'_14) -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T__'8866'_14) -> T__'8866'_14 -> T__'8866'_14
du_sub_396 (((AgdaAny -> T__'8866'_14) -> Maybe AgdaAny -> T__'8866'_14)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T__'8866'_14) -> Maybe AgdaAny -> T__'8866'_14
du_lifts_378 ((AgdaAny -> T__'8866'_14) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8866'_14
v0)) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2))
      MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v2 T__'8866'_14
v3
        -> (T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
             T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
             (((AgdaAny -> T__'8866'_14) -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T__'8866'_14) -> T__'8866'_14 -> T__'8866'_14
du_sub_396 ((AgdaAny -> T__'8866'_14) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8866'_14
v0) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2))
             (((AgdaAny -> T__'8866'_14) -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T__'8866'_14) -> T__'8866'_14 -> T__'8866'_14
du_sub_396 ((AgdaAny -> T__'8866'_14) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8866'_14
v0) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v3))
      MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v2
        -> (T__'8866'_14 -> T__'8866'_14) -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
             T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_force_24 (((AgdaAny -> T__'8866'_14) -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T__'8866'_14) -> T__'8866'_14 -> T__'8866'_14
du_sub_396 ((AgdaAny -> T__'8866'_14) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8866'_14
v0) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2))
      MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v2
        -> (T__'8866'_14 -> T__'8866'_14) -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
             T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_delay_26 (((AgdaAny -> T__'8866'_14) -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T__'8866'_14) -> T__'8866'_14 -> T__'8866'_14
du_sub_396 ((AgdaAny -> T__'8866'_14) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8866'_14
v0) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2))
      MAlonzo.Code.Untyped.C_con_28 T_TmCon_198
v2 -> T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1
      MAlonzo.Code.Untyped.C_constr_34 Integer
v2 [T__'8866'_14]
v3
        -> (Integer -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
             Integer -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_constr_34 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2)
             (((AgdaAny -> T__'8866'_14) -> [T__'8866'_14] -> [T__'8866'_14])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T__'8866'_14) -> [T__'8866'_14] -> [T__'8866'_14]
du_subList_390 ((AgdaAny -> T__'8866'_14) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8866'_14
v0) ([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v3))
      MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v2 [T__'8866'_14]
v3
        -> (T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
             T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40 (((AgdaAny -> T__'8866'_14) -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T__'8866'_14) -> T__'8866'_14 -> T__'8866'_14
du_sub_396 ((AgdaAny -> T__'8866'_14) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8866'_14
v0) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2))
             (((AgdaAny -> T__'8866'_14) -> [T__'8866'_14] -> [T__'8866'_14])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T__'8866'_14) -> [T__'8866'_14] -> [T__'8866'_14]
du_subList_390 ((AgdaAny -> T__'8866'_14) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8866'_14
v0) ([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v3))
      MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v2 -> T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1
      T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 -> T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1
      T__'8866'_14
_ -> T__'8866'_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.RenamingSubstitution.extend
d_extend_454 ::
  () ->
  () ->
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  Maybe AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14
d_extend_454 :: ()
-> ()
-> (AgdaAny -> T__'8866'_14)
-> T__'8866'_14
-> Maybe AgdaAny
-> T__'8866'_14
d_extend_454 ~()
v0 ~()
v1 AgdaAny -> T__'8866'_14
v2 T__'8866'_14
v3 Maybe AgdaAny
v4 = (AgdaAny -> T__'8866'_14)
-> T__'8866'_14 -> Maybe AgdaAny -> T__'8866'_14
du_extend_454 AgdaAny -> T__'8866'_14
v2 T__'8866'_14
v3 Maybe AgdaAny
v4
du_extend_454 ::
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  Maybe AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14
du_extend_454 :: (AgdaAny -> T__'8866'_14)
-> T__'8866'_14 -> Maybe AgdaAny -> T__'8866'_14
du_extend_454 AgdaAny -> T__'8866'_14
v0 T__'8866'_14
v1 Maybe AgdaAny
v2
  = case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v2 of
      MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v3 -> (AgdaAny -> T__'8866'_14) -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe AgdaAny -> T__'8866'_14
v0 AgdaAny
v3
      Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1
      Maybe AgdaAny
_ -> T__'8866'_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.RenamingSubstitution._[_]
d__'91'_'93'_468 ::
  () ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14
d__'91'_'93'_468 :: () -> T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
d__'91'_'93'_468 ~()
v0 T__'8866'_14
v1 T__'8866'_14
v2 = T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
du__'91'_'93'_468 T__'8866'_14
v1 T__'8866'_14
v2
du__'91'_'93'_468 ::
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14
du__'91'_'93'_468 :: T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
du__'91'_'93'_468 T__'8866'_14
v0 T__'8866'_14
v1
  = ((AgdaAny -> T__'8866'_14) -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
      (AgdaAny -> T__'8866'_14) -> T__'8866'_14 -> T__'8866'_14
du_sub_396
      (((AgdaAny -> T__'8866'_14)
 -> T__'8866'_14 -> Maybe AgdaAny -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T__'8866'_14)
-> T__'8866'_14 -> Maybe AgdaAny -> T__'8866'_14
du_extend_454 ((AgdaAny -> T__'8866'_14) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v1))
      (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v0)
-- Untyped.RenamingSubstitution.lifts-cong
d_lifts'45'cong_486 ::
  () ->
  () ->
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lifts'45'cong_486 :: ()
-> ()
-> (AgdaAny -> T__'8866'_14)
-> (AgdaAny -> T__'8866'_14)
-> (AgdaAny -> T__'8801'__12)
-> Maybe AgdaAny
-> T__'8801'__12
d_lifts'45'cong_486 = ()
-> ()
-> (AgdaAny -> T__'8866'_14)
-> (AgdaAny -> T__'8866'_14)
-> (AgdaAny -> T__'8801'__12)
-> Maybe AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Untyped.RenamingSubstitution.subList-cong
d_subList'45'cong_506 ::
  () ->
  () ->
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subList'45'cong_506 :: ()
-> ()
-> (AgdaAny -> T__'8866'_14)
-> (AgdaAny -> T__'8866'_14)
-> (AgdaAny -> T__'8801'__12)
-> [T__'8866'_14]
-> T__'8801'__12
d_subList'45'cong_506 = ()
-> ()
-> (AgdaAny -> T__'8866'_14)
-> (AgdaAny -> T__'8866'_14)
-> (AgdaAny -> T__'8801'__12)
-> [T__'8866'_14]
-> T__'8801'__12
forall a. a
erased
-- Untyped.RenamingSubstitution.sub-cong
d_sub'45'cong_520 ::
  () ->
  () ->
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_sub'45'cong_520 :: ()
-> ()
-> (AgdaAny -> T__'8866'_14)
-> (AgdaAny -> T__'8866'_14)
-> (AgdaAny -> T__'8801'__12)
-> T__'8866'_14
-> T__'8801'__12
d_sub'45'cong_520 = ()
-> ()
-> (AgdaAny -> T__'8866'_14)
-> (AgdaAny -> T__'8866'_14)
-> (AgdaAny -> T__'8801'__12)
-> T__'8866'_14
-> T__'8801'__12
forall a. a
erased
-- Untyped.RenamingSubstitution.lifts-id
d_lifts'45'id_578 ::
  () ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lifts'45'id_578 :: () -> Maybe AgdaAny -> T__'8801'__12
d_lifts'45'id_578 = () -> Maybe AgdaAny -> T__'8801'__12
forall a. a
erased
-- Untyped.RenamingSubstitution.subList-id
d_subList'45'id_586 ::
  () ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subList'45'id_586 :: () -> [T__'8866'_14] -> T__'8801'__12
d_subList'45'id_586 = () -> [T__'8866'_14] -> T__'8801'__12
forall a. a
erased
-- Untyped.RenamingSubstitution.sub-id
d_sub'45'id_592 ::
  () ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_sub'45'id_592 :: () -> T__'8866'_14 -> T__'8801'__12
d_sub'45'id_592 = () -> T__'8866'_14 -> T__'8801'__12
forall a. a
erased
-- Untyped.RenamingSubstitution.lifts-lift
d_lifts'45'lift_634 ::
  () ->
  () ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lifts'45'lift_634 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8866'_14)
-> Maybe AgdaAny
-> T__'8801'__12
d_lifts'45'lift_634 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8866'_14)
-> Maybe AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Untyped.RenamingSubstitution.subList-ren
d_subList'45'ren_658 ::
  () ->
  () ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subList'45'ren_658 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8866'_14)
-> [T__'8866'_14]
-> T__'8801'__12
d_subList'45'ren_658 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8866'_14)
-> [T__'8866'_14]
-> T__'8801'__12
forall a. a
erased
-- Untyped.RenamingSubstitution.sub-ren
d_sub'45'ren_672 ::
  () ->
  () ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_sub'45'ren_672 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8866'_14)
-> T__'8866'_14
-> T__'8801'__12
d_sub'45'ren_672 = ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8866'_14)
-> T__'8866'_14
-> T__'8801'__12
forall a. a
erased
-- Untyped.RenamingSubstitution.ren-lift-lifts
d_ren'45'lift'45'lifts_762 ::
  () ->
  () ->
  () ->
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  (AgdaAny -> AgdaAny) ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_ren'45'lift'45'lifts_762 :: ()
-> ()
-> ()
-> (AgdaAny -> T__'8866'_14)
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T__'8801'__12
d_ren'45'lift'45'lifts_762 = ()
-> ()
-> ()
-> (AgdaAny -> T__'8866'_14)
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Untyped.RenamingSubstitution.renList-sub
d_renList'45'sub_786 ::
  () ->
  () ->
  () ->
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  (AgdaAny -> AgdaAny) ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_renList'45'sub_786 :: ()
-> ()
-> ()
-> (AgdaAny -> T__'8866'_14)
-> (AgdaAny -> AgdaAny)
-> [T__'8866'_14]
-> T__'8801'__12
d_renList'45'sub_786 = ()
-> ()
-> ()
-> (AgdaAny -> T__'8866'_14)
-> (AgdaAny -> AgdaAny)
-> [T__'8866'_14]
-> T__'8801'__12
forall a. a
erased
-- Untyped.RenamingSubstitution.ren-sub
d_ren'45'sub_800 ::
  () ->
  () ->
  () ->
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_ren'45'sub_800 :: ()
-> ()
-> ()
-> (AgdaAny -> T__'8866'_14)
-> (AgdaAny -> AgdaAny)
-> T__'8866'_14
-> T__'8801'__12
d_ren'45'sub_800 = ()
-> ()
-> ()
-> (AgdaAny -> T__'8866'_14)
-> (AgdaAny -> AgdaAny)
-> T__'8866'_14
-> T__'8801'__12
forall a. a
erased
-- Untyped.RenamingSubstitution.lifts-comp
d_lifts'45'comp_890 ::
  () ->
  () ->
  () ->
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lifts'45'comp_890 :: ()
-> ()
-> ()
-> (AgdaAny -> T__'8866'_14)
-> (AgdaAny -> T__'8866'_14)
-> Maybe AgdaAny
-> T__'8801'__12
d_lifts'45'comp_890 = ()
-> ()
-> ()
-> (AgdaAny -> T__'8866'_14)
-> (AgdaAny -> T__'8866'_14)
-> Maybe AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Untyped.RenamingSubstitution.subList-comp
d_subList'45'comp_914 ::
  () ->
  () ->
  () ->
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subList'45'comp_914 :: ()
-> ()
-> ()
-> (AgdaAny -> T__'8866'_14)
-> (AgdaAny -> T__'8866'_14)
-> [T__'8866'_14]
-> T__'8801'__12
d_subList'45'comp_914 = ()
-> ()
-> ()
-> (AgdaAny -> T__'8866'_14)
-> (AgdaAny -> T__'8866'_14)
-> [T__'8866'_14]
-> T__'8801'__12
forall a. a
erased
-- Untyped.RenamingSubstitution.sub-comp
d_sub'45'comp_928 ::
  () ->
  () ->
  () ->
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  (AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14) ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_sub'45'comp_928 :: ()
-> ()
-> ()
-> (AgdaAny -> T__'8866'_14)
-> (AgdaAny -> T__'8866'_14)
-> T__'8866'_14
-> T__'8801'__12
d_sub'45'comp_928 = ()
-> ()
-> ()
-> (AgdaAny -> T__'8866'_14)
-> (AgdaAny -> T__'8866'_14)
-> T__'8866'_14
-> T__'8801'__12
forall a. a
erased