{-# 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.Data.Fin.Base
import qualified MAlonzo.Code.Untyped

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