{-# 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.Induction.WellFounded 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.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Induction

-- Induction.WellFounded.WfRec
d_WfRec_22 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) -> AgdaAny -> ()
d_WfRec_22 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Level_18
d_WfRec_22 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Induction.WellFounded.Acc
d_Acc_42 :: p -> p -> p -> p -> p -> T_Level_18
d_Acc_42 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
data T_Acc_42 = C_acc_52
-- Induction.WellFounded.WellFounded
d_WellFounded_54 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) -> ()
d_WellFounded_54 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
d_WellFounded_54 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
forall a. a
erased
-- Induction.WellFounded.acc-inverse
d_acc'45'inverse_66 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny -> T_Acc_42 -> AgdaAny -> AgdaAny -> T_Acc_42
d_acc'45'inverse_66 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Acc_42
-> AgdaAny
-> AgdaAny
-> T_Acc_42
d_acc'45'inverse_66 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Acc_42
-> AgdaAny
-> AgdaAny
-> T_Acc_42
forall a. a
erased
-- Induction.WellFounded._.Acc-resp-flip-≈
d_Acc'45'resp'45'flip'45''8776'_86 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> T_Acc_42 -> T_Acc_42
d_Acc'45'resp'45'flip'45''8776'_86 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
d_Acc'45'resp'45'flip'45''8776'_86 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
forall a. a
erased
-- Induction.WellFounded._.Acc-resp-≈
d_Acc'45'resp'45''8776'_96 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> T_Acc_42 -> T_Acc_42
d_Acc'45'resp'45''8776'_96 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
d_Acc'45'resp'45''8776'_96 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
forall a. a
erased
-- Induction.WellFounded.Some.wfRecBuilder
d_wfRecBuilder_116 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
  AgdaAny -> T_Acc_42 -> AgdaAny -> AgdaAny -> AgdaAny
d_wfRecBuilder_116 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_wfRecBuilder_116 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v6 ~AgdaAny
v7 ~T_Acc_42
v8 AgdaAny
v9 ~AgdaAny
v10
  = (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny
du_wfRecBuilder_116 AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v6 AgdaAny
v9
du_wfRecBuilder_116 ::
  (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
  AgdaAny -> AgdaAny
du_wfRecBuilder_116 :: (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny
du_wfRecBuilder_116 AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v0 AgdaAny
v1
  = (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v0 AgdaAny
v1 (\ AgdaAny
v2 AgdaAny
v3 -> ((AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny
du_wfRecBuilder_116 ((AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v0) AgdaAny
v2)
-- Induction.WellFounded.Some.wfRec
d_wfRec_128 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
  AgdaAny -> T_Acc_42 -> AgdaAny
d_wfRec_128 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> AgdaAny
d_wfRec_128 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 = (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> AgdaAny
du_wfRec_128
du_wfRec_128 ::
  (AgdaAny -> ()) ->
  (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
  AgdaAny -> T_Acc_42 -> AgdaAny
du_wfRec_128 :: (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> AgdaAny
du_wfRec_128
  = (((AgdaAny -> T_Level_18)
  -> (AgdaAny -> AgdaAny -> AgdaAny)
  -> AgdaAny
  -> AgdaAny
  -> AgdaAny)
 -> (AgdaAny -> T_Level_18)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> AgdaAny
forall a b. a -> b
coe
      ((AgdaAny -> T_Level_18)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Induction.du_subsetBuild_62
      (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 -> ((AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny
du_wfRecBuilder_116 AgdaAny
v1 AgdaAny
v4)
-- Induction.WellFounded.Some.unfold-wfRec
d_unfold'45'wfRec_140 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
  AgdaAny ->
  T_Acc_42 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_unfold'45'wfRec_140 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> T__'8801'__12
d_unfold'45'wfRec_140 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> T__'8801'__12
forall a. a
erased
-- Induction.WellFounded.All.wfRecBuilder
d_wfRecBuilder_160 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> T_Acc_42) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_wfRecBuilder_160 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_wfRecBuilder_160 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> T_Acc_42
v4 ~T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v7 ~AgdaAny
v8 AgdaAny
v9
  = (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
du_wfRecBuilder_160 AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v7 AgdaAny
v9
du_wfRecBuilder_160 ::
  (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny
du_wfRecBuilder_160 :: (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
du_wfRecBuilder_160 AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2
  = ((AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny
du_wfRecBuilder_116 ((AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
-- Induction.WellFounded.All.wfRec
d_wfRec_168 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> T_Acc_42) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
  AgdaAny -> AgdaAny
d_wfRec_168 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_wfRec_168 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> T_Acc_42
v4 ~T_Level_18
v5 = (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_wfRec_168
du_wfRec_168 ::
  (AgdaAny -> ()) ->
  (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
  AgdaAny -> AgdaAny
du_wfRec_168 :: (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_wfRec_168
  = (((AgdaAny -> T_Level_18)
  -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> T_Level_18)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      ((AgdaAny -> T_Level_18)
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Induction.du_build_36
      (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> ((AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
du_wfRecBuilder_160 AgdaAny
v1 AgdaAny
v3)
-- Induction.WellFounded.All.wfRec-builder
d_wfRec'45'builder_170 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> T_Acc_42) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_wfRec'45'builder_170 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_wfRec'45'builder_170 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> T_Acc_42
v4 ~T_Level_18
v5
  = (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_wfRec'45'builder_170
du_wfRec'45'builder_170 ::
  (AgdaAny -> ()) ->
  (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_wfRec'45'builder_170 :: (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_wfRec'45'builder_170 AgdaAny -> T_Level_18
v0 AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 = ((AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
du_wfRecBuilder_160 AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v1 AgdaAny
v3
-- Induction.WellFounded.FixPoint.some-wfrec-Irrelevant
d_some'45'wfrec'45'Irrelevant_200 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> T_Acc_42) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> 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) ->
  AgdaAny -> ()
d_some'45'wfrec'45'Irrelevant_200 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> (AgdaAny
    -> (AgdaAny -> AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny -> T__'8801'__12)
    -> T__'8801'__12)
-> AgdaAny
-> T_Level_18
d_some'45'wfrec'45'Irrelevant_200 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> (AgdaAny
    -> (AgdaAny -> AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny -> T__'8801'__12)
    -> T__'8801'__12)
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Induction.WellFounded.FixPoint.some-wfRec-irrelevant
d_some'45'wfRec'45'irrelevant_210 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> T_Acc_42) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> 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) ->
  AgdaAny ->
  T_Acc_42 ->
  T_Acc_42 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_some'45'wfRec'45'irrelevant_210 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> (AgdaAny
    -> (AgdaAny -> AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny -> T__'8801'__12)
    -> T__'8801'__12)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
-> T__'8801'__12
d_some'45'wfRec'45'irrelevant_210 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> (AgdaAny
    -> (AgdaAny -> AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny -> T__'8801'__12)
    -> T__'8801'__12)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
-> T__'8801'__12
forall a. a
erased
-- Induction.WellFounded.FixPoint._.wfRec
d_wfRec_226 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> T_Acc_42) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> 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) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
  AgdaAny -> AgdaAny
d_wfRec_226 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> (AgdaAny
    -> (AgdaAny -> AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny -> T__'8801'__12)
    -> T__'8801'__12)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_wfRec_226 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Acc_42
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v7 ~AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12)
-> T__'8801'__12
v8 = (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_wfRec_226
du_wfRec_226 ::
  (AgdaAny -> ()) ->
  (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
  AgdaAny -> AgdaAny
du_wfRec_226 :: (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_wfRec_226 = ((AgdaAny -> T_Level_18)
 -> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_wfRec_168
-- Induction.WellFounded.FixPoint._.wfRec-builder
d_wfRec'45'builder_228 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> T_Acc_42) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> 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) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_wfRec'45'builder_228 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> (AgdaAny
    -> (AgdaAny -> AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny -> T__'8801'__12)
    -> T__'8801'__12)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_wfRec'45'builder_228 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Acc_42
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v7 ~AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12)
-> T__'8801'__12
v8
  = (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_wfRec'45'builder_228
du_wfRec'45'builder_228 ::
  (AgdaAny -> ()) ->
  (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_wfRec'45'builder_228 :: (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_wfRec'45'builder_228 = ((AgdaAny -> T_Level_18)
 -> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_wfRec'45'builder_170
-- Induction.WellFounded.FixPoint._.wfRecBuilder
d_wfRecBuilder_230 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> T_Acc_42) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> 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) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_wfRecBuilder_230 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> (AgdaAny
    -> (AgdaAny -> AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny -> T__'8801'__12)
    -> T__'8801'__12)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_wfRecBuilder_230 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Acc_42
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v7 ~AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12)
-> T__'8801'__12
v8
  = (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_wfRecBuilder_230
du_wfRecBuilder_230 ::
  (AgdaAny -> ()) ->
  (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_wfRecBuilder_230 :: (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_wfRecBuilder_230 AgdaAny -> T_Level_18
v0 AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 = ((AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
du_wfRecBuilder_160 AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v1 AgdaAny
v3
-- Induction.WellFounded.FixPoint.wfRecBuilder-wfRec
d_wfRecBuilder'45'wfRec_238 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> T_Acc_42) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> 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) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_wfRecBuilder'45'wfRec_238 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> (AgdaAny
    -> (AgdaAny -> AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny -> T__'8801'__12)
    -> T__'8801'__12)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
d_wfRecBuilder'45'wfRec_238 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> (AgdaAny
    -> (AgdaAny -> AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny -> T__'8801'__12)
    -> T__'8801'__12)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Induction.WellFounded.FixPoint.unfold-wfRec
d_unfold'45'wfRec_256 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> T_Acc_42) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> 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) ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_unfold'45'wfRec_256 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> (AgdaAny
    -> (AgdaAny -> AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny -> T__'8801'__12)
    -> T__'8801'__12)
-> AgdaAny
-> T__'8801'__12
d_unfold'45'wfRec_256 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> (AgdaAny
    -> (AgdaAny -> AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny -> AgdaAny)
    -> (AgdaAny -> AgdaAny -> T__'8801'__12)
    -> T__'8801'__12)
-> AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Induction.WellFounded._.acc⇒asym
d_acc'8658'asym_274 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny ->
  AgdaAny ->
  T_Acc_42 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_acc'8658'asym_274 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> AgdaAny
-> AgdaAny
-> T_Irrelevant_20
d_acc'8658'asym_274 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> AgdaAny
-> AgdaAny
-> T_Irrelevant_20
forall a. a
erased
-- Induction.WellFounded._.wf⇒asym
d_wf'8658'asym_292 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> T_Acc_42) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_wf'8658'asym_292 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Irrelevant_20
d_wf'8658'asym_292 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Irrelevant_20
forall a. a
erased
-- Induction.WellFounded._.wf⇒irrefl
d_wf'8658'irrefl_298 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> T_Acc_42) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_wf'8658'irrefl_298 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Irrelevant_20
d_wf'8658'irrefl_298 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Irrelevant_20
forall a. a
erased
-- Induction.WellFounded.Subrelation.accessible
d_accessible_324 ::
  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 -> T_Acc_42 -> T_Acc_42
d_accessible_324 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
d_accessible_324 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
forall a. a
erased
-- Induction.WellFounded.Subrelation.wellFounded
d_wellFounded_330 ::
  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 -> T_Acc_42) -> AgdaAny -> T_Acc_42
d_wellFounded_330 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
d_wellFounded_330 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
forall a. a
erased
-- Induction.WellFounded.InverseImage.accessible
d_accessible_350 ::
  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 -> T_Acc_42 -> T_Acc_42
d_accessible_350 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
d_accessible_350 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
forall a. a
erased
-- Induction.WellFounded.InverseImage.wellFounded
d_wellFounded_356 ::
  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 -> T_Acc_42) -> AgdaAny -> T_Acc_42
d_wellFounded_356 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
d_wellFounded_356 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
forall a. a
erased
-- Induction.WellFounded.InverseImage.well-founded
d_well'45'founded_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 -> T_Acc_42) -> AgdaAny -> T_Acc_42
d_well'45'founded_362 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
d_well'45'founded_362 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
forall a. a
erased
-- Induction.WellFounded.TransitiveClosure._<⁺_
d__'60''8314'__374 :: p -> p -> p -> p -> p -> p -> T_Level_18
d__'60''8314'__374 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T__'60''8314'__374
  = C_'91'_'93'_382 AgdaAny |
    C_trans_394 AgdaAny T__'60''8314'__374 T__'60''8314'__374
-- Induction.WellFounded.TransitiveClosure.downwardsClosed
d_downwardsClosed_400 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny -> AgdaAny -> T_Acc_42 -> T__'60''8314'__374 -> T_Acc_42
d_downwardsClosed_400 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> T__'60''8314'__374
-> T_Acc_42
d_downwardsClosed_400 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> T__'60''8314'__374
-> T_Acc_42
forall a. a
erased
-- Induction.WellFounded.TransitiveClosure.accessible
d_accessible_410 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> T_Acc_42 -> T_Acc_42
d_accessible_410 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
d_accessible_410 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
forall a. a
erased
-- Induction.WellFounded.TransitiveClosure.accessible′
d_accessible'8242'_414 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny -> T_Acc_42 -> AgdaAny -> T__'60''8314'__374 -> T_Acc_42
d_accessible'8242'_414 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Acc_42
-> AgdaAny
-> T__'60''8314'__374
-> T_Acc_42
d_accessible'8242'_414 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Acc_42
-> AgdaAny
-> T__'60''8314'__374
-> T_Acc_42
forall a. a
erased
-- Induction.WellFounded.TransitiveClosure.wellFounded
d_wellFounded_428 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> T_Acc_42) -> AgdaAny -> T_Acc_42
d_wellFounded_428 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
d_wellFounded_428 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
forall a. a
erased
-- Induction.WellFounded.Lexicographic._<_
d__'60'__454 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> T_Level_18
d__'60'__454 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8 p
a9 = ()
data T__'60'__454 = C_left_466 AgdaAny | C_right_476 AgdaAny
-- Induction.WellFounded.Lexicographic.accessible
d_accessible_484 ::
  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 -> T_Acc_42 -> (AgdaAny -> AgdaAny -> T_Acc_42) -> T_Acc_42
d_accessible_484 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> (AgdaAny -> AgdaAny -> T_Acc_42)
-> T_Acc_42
d_accessible_484 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> (AgdaAny -> AgdaAny -> T_Acc_42)
-> T_Acc_42
forall a. a
erased
-- Induction.WellFounded.Lexicographic.accessible′
d_accessible'8242'_492 ::
  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 ->
  T_Acc_42 ->
  T_Acc_42 ->
  (AgdaAny -> AgdaAny -> T_Acc_42) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T__'60'__454 -> T_Acc_42
d_accessible'8242'_492 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
-> (AgdaAny -> AgdaAny -> T_Acc_42)
-> T_Σ_14
-> T__'60'__454
-> T_Acc_42
d_accessible'8242'_492 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
-> (AgdaAny -> AgdaAny -> T_Acc_42)
-> T_Σ_14
-> T__'60'__454
-> T_Acc_42
forall a. a
erased
-- Induction.WellFounded.Lexicographic.wellFounded
d_wellFounded_514 ::
  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 -> T_Acc_42) ->
  (AgdaAny -> AgdaAny -> T_Acc_42) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_Acc_42
d_wellFounded_514 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> AgdaAny -> T_Acc_42)
-> T_Σ_14
-> T_Acc_42
d_wellFounded_514 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> AgdaAny -> T_Acc_42)
-> T_Σ_14
-> T_Acc_42
forall a. a
erased
-- Induction.WellFounded.Lexicographic.well-founded
d_well'45'founded_522 ::
  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 -> T_Acc_42) ->
  (AgdaAny -> AgdaAny -> T_Acc_42) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_Acc_42
d_well'45'founded_522 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> AgdaAny -> T_Acc_42)
-> T_Σ_14
-> T_Acc_42
d_well'45'founded_522 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> AgdaAny -> T_Acc_42)
-> T_Σ_14
-> T_Acc_42
forall a. a
erased
-- Induction.WellFounded.Inverse-image.accessible
d_accessible_526 ::
  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 -> T_Acc_42 -> T_Acc_42
d_accessible_526 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
d_accessible_526 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
forall a. a
erased
-- Induction.WellFounded.Inverse-image.well-founded
d_well'45'founded_528 ::
  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 -> T_Acc_42) -> AgdaAny -> T_Acc_42
d_well'45'founded_528 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
d_well'45'founded_528 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
forall a. a
erased
-- Induction.WellFounded.Inverse-image.wellFounded
d_wellFounded_530 ::
  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 -> T_Acc_42) -> AgdaAny -> T_Acc_42
d_wellFounded_530 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
d_wellFounded_530 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
forall a. a
erased
-- Induction.WellFounded.Transitive-closure._<⁺_
d__'60''8314'__534 :: p -> p -> p -> p -> p -> p -> T_Level_18
d__'60''8314'__534 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Induction.WellFounded.Transitive-closure.accessible
d_accessible_538 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> T_Acc_42 -> T_Acc_42
d_accessible_538 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
d_accessible_538 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
forall a. a
erased
-- Induction.WellFounded.Transitive-closure.accessible′
d_accessible'8242'_540 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny -> T_Acc_42 -> AgdaAny -> T__'60''8314'__374 -> T_Acc_42
d_accessible'8242'_540 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Acc_42
-> AgdaAny
-> T__'60''8314'__374
-> T_Acc_42
d_accessible'8242'_540 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Acc_42
-> AgdaAny
-> T__'60''8314'__374
-> T_Acc_42
forall a. a
erased
-- Induction.WellFounded.Transitive-closure.downwardsClosed
d_downwardsClosed_542 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny -> AgdaAny -> T_Acc_42 -> T__'60''8314'__374 -> T_Acc_42
d_downwardsClosed_542 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> T__'60''8314'__374
-> T_Acc_42
d_downwardsClosed_542 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> T__'60''8314'__374
-> T_Acc_42
forall a. a
erased
-- Induction.WellFounded.Transitive-closure.wellFounded
d_wellFounded_546 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> T_Acc_42) -> AgdaAny -> T_Acc_42
d_wellFounded_546 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
d_wellFounded_546 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
forall a. a
erased
-- Induction.WellFounded..generalizedField-A.a
d_'46'generalizedField'45'A'46'a_6161 ::
  T_GeneralizeTel_6167 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'A'46'a_6161 :: T_GeneralizeTel_6167 -> T_Level_18
d_'46'generalizedField'45'A'46'a_6161 T_GeneralizeTel_6167
v0
  = case T_GeneralizeTel_6167 -> T_GeneralizeTel_6167
forall a b. a -> b
coe T_GeneralizeTel_6167
v0 of
      C_mkGeneralizeTel_6169 T_Level_18
v1 T_Level_18
v3 -> T_Level_18 -> T_Level_18
forall a b. a -> b
coe T_Level_18
v1
      T_GeneralizeTel_6167
_ -> T_Level_18
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Induction.WellFounded..generalizedField-A
d_'46'generalizedField'45'A_6163 :: T_GeneralizeTel_6167 -> ()
d_'46'generalizedField'45'A_6163 :: T_GeneralizeTel_6167 -> T_Level_18
d_'46'generalizedField'45'A_6163 = T_GeneralizeTel_6167 -> T_Level_18
forall a. a
erased
-- Induction.WellFounded..generalizedField-r
d_'46'generalizedField'45'r_6165 ::
  T_GeneralizeTel_6167 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'r_6165 :: T_GeneralizeTel_6167 -> T_Level_18
d_'46'generalizedField'45'r_6165 T_GeneralizeTel_6167
v0
  = case T_GeneralizeTel_6167 -> T_GeneralizeTel_6167
forall a b. a -> b
coe T_GeneralizeTel_6167
v0 of
      C_mkGeneralizeTel_6169 T_Level_18
v1 T_Level_18
v3 -> T_Level_18 -> T_Level_18
forall a b. a -> b
coe T_Level_18
v3
      T_GeneralizeTel_6167
_ -> T_Level_18
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Induction.WellFounded.GeneralizeTel
d_GeneralizeTel_6167 :: T_Level_18
d_GeneralizeTel_6167 = ()
data T_GeneralizeTel_6167
  = C_mkGeneralizeTel_6169 MAlonzo.Code.Agda.Primitive.T_Level_18
                           MAlonzo.Code.Agda.Primitive.T_Level_18
-- Induction.WellFounded..generalizedField-A.a
d_'46'generalizedField'45'A'46'a_10101 ::
  T_GeneralizeTel_10107 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'A'46'a_10101 :: T_GeneralizeTel_10107 -> T_Level_18
d_'46'generalizedField'45'A'46'a_10101 T_GeneralizeTel_10107
v0
  = case T_GeneralizeTel_10107 -> T_GeneralizeTel_10107
forall a b. a -> b
coe T_GeneralizeTel_10107
v0 of
      C_mkGeneralizeTel_10109 T_Level_18
v1 T_Level_18
v3 -> T_Level_18 -> T_Level_18
forall a b. a -> b
coe T_Level_18
v1
      T_GeneralizeTel_10107
_ -> T_Level_18
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Induction.WellFounded..generalizedField-A
d_'46'generalizedField'45'A_10103 :: T_GeneralizeTel_10107 -> ()
d_'46'generalizedField'45'A_10103 :: T_GeneralizeTel_10107 -> T_Level_18
d_'46'generalizedField'45'A_10103 = T_GeneralizeTel_10107 -> T_Level_18
forall a. a
erased
-- Induction.WellFounded..generalizedField-r
d_'46'generalizedField'45'r_10105 ::
  T_GeneralizeTel_10107 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'r_10105 :: T_GeneralizeTel_10107 -> T_Level_18
d_'46'generalizedField'45'r_10105 T_GeneralizeTel_10107
v0
  = case T_GeneralizeTel_10107 -> T_GeneralizeTel_10107
forall a b. a -> b
coe T_GeneralizeTel_10107
v0 of
      C_mkGeneralizeTel_10109 T_Level_18
v1 T_Level_18
v3 -> T_Level_18 -> T_Level_18
forall a b. a -> b
coe T_Level_18
v3
      T_GeneralizeTel_10107
_ -> T_Level_18
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Induction.WellFounded.GeneralizeTel
d_GeneralizeTel_10107 :: T_Level_18
d_GeneralizeTel_10107 = ()
data T_GeneralizeTel_10107
  = C_mkGeneralizeTel_10109 MAlonzo.Code.Agda.Primitive.T_Level_18
                            MAlonzo.Code.Agda.Primitive.T_Level_18