plutus-metatheory-1.70.0.0: Command line tool for running plutus core programs

Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple

Documentation

d__IsRelatedTo__78 ∷ p → p → p → p → p → p → p → p → p → p → p → p → p → p → p → p → p → () Source #

data T__IsRelatedTo__78 Source #

Constructors

C_strict_86 AgdaAny
C_nonstrict_90 AgdaAny
C_equals_94 AgdaAny

d_start_96 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__IsRelatedTo__78 → AgdaAny Source #

du_start_96 ∷ T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__IsRelatedTo__78 → AgdaAny Source #

d_'8801''45'go_104 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__IsRelatedTo__78 → T__IsRelatedTo__78 Source #

du_'8801''45'go_104 ∷ T__IsRelatedTo__78 → T__IsRelatedTo__78 Source #

d_'46'extendedlambda0_110 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_'46'extendedlambda0_110 ∷ AgdaAny → AgdaAny Source #

d_'46'extendedlambda1_116 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_'46'extendedlambda1_116 ∷ AgdaAny → AgdaAny Source #

d_'46'extendedlambda2_122 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_'46'extendedlambda2_122 ∷ AgdaAny → AgdaAny Source #

d_'8776''45'go_124 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → T__IsRelatedTo__78 Source #

du_'8776''45'go_124 ∷ T_IsPreorder_76 → T_Σ_14 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → T__IsRelatedTo__78 Source #

d_'8804''45'go_138 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → T__IsRelatedTo__78 Source #

du_'8804''45'go_138 ∷ T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → T__IsRelatedTo__78 Source #

d_'60''45'go_152 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → T__IsRelatedTo__78 Source #

du_'60''45'go_152 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → T__IsRelatedTo__78 Source #

d_stop_166 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T__IsRelatedTo__78 Source #

du_stop_166 ∷ T_IsPreorder_76 → AgdaAny → T__IsRelatedTo__78 Source #

d_IsStrict_172 ∷ p → p → p → p → p → p → p → p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsStrict_172 Source #

Constructors

d_IsStrict'63'_188 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__IsRelatedTo__78 → T_Dec_20 Source #

du_IsStrict'63'_188 ∷ T__IsRelatedTo__78 → T_Dec_20 Source #

d_extractStrict_198 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__IsRelatedTo__78 → T_IsStrict_172 → AgdaAny Source #

du_extractStrict_198 ∷ T__IsRelatedTo__78 → T_IsStrict_172 → AgdaAny Source #

d_strictRelation_202 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_SubRelation_60 Source #

du_strictRelation_202 ∷ T_SubRelation_60 Source #

d_IsEquality_208 ∷ p → p → p → p → p → p → p → p → p → p → p → p → p → p → p → p → p → p → () Source #

data T_IsEquality_208 Source #

Constructors

C_isEquality_216

d_IsEquality'63'_224 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__IsRelatedTo__78 → T_Dec_20 Source #

du_IsEquality'63'_224 ∷ T__IsRelatedTo__78 → T_Dec_20 Source #

d_extractEquality_234 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__IsRelatedTo__78 → T_IsEquality_208 → AgdaAny Source #

du_extractEquality_234 ∷ T__IsRelatedTo__78 → T_IsEquality_208 → AgdaAny Source #

d_eqRelation_238 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_SubRelation_60 Source #

du_eqRelation_238 ∷ T_SubRelation_60 Source #

d_begin__242 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__IsRelatedTo__78 → AgdaAny Source #

du_begin__242 ∷ T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__IsRelatedTo__78 → AgdaAny Source #

d_begin__246 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__IsRelatedTo__78 → AgdaAny → AgdaAny Source #

du_begin__246 ∷ AgdaAny → AgdaAny → T__IsRelatedTo__78 → AgdaAny → AgdaAny Source #

d_begin__250 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__IsRelatedTo__78 → AgdaAny → AgdaAny Source #

du_begin__250 ∷ AgdaAny → AgdaAny → T__IsRelatedTo__78 → AgdaAny → AgdaAny Source #

d_begin'45'contradiction__254 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T__IsRelatedTo__78 → AgdaAny → T_Level_18 → () → AgdaAny Source #

du_begin'45'contradiction__254 ∷ AgdaAny → T__IsRelatedTo__78 → AgdaAny → T_Level_18 → () → AgdaAny Source #

d_step'45''8801'_258 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → T__'8801'__12 → T__IsRelatedTo__78 Source #

du_step'45''8801'_258 ∷ AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → T__'8801'__12 → T__IsRelatedTo__78 Source #

d_step'45''8801''45''8739'_260 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__IsRelatedTo__78 → T__IsRelatedTo__78 Source #

du_step'45''8801''45''8739'_260 ∷ T__IsRelatedTo__78 → T__IsRelatedTo__78 Source #

d_step'45''8801''45''10216'_262 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → T__'8801'__12 → T__IsRelatedTo__78 Source #

du_step'45''8801''45''10216'_262 ∷ AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → T__'8801'__12 → T__IsRelatedTo__78 Source #

d_step'45''8801''45''10217'_264 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → T__'8801'__12 → T__IsRelatedTo__78 Source #

du_step'45''8801''45''10217'_264 ∷ AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → T__'8801'__12 → T__IsRelatedTo__78 Source #

d_step'45''8801''728'_266 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → T__'8801'__12 → T__IsRelatedTo__78 Source #

du_step'45''8801''728'_266 ∷ AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → T__'8801'__12 → T__IsRelatedTo__78 Source #

d_step'45''8776'_270 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → AgdaAny → T__IsRelatedTo__78 Source #

du_step'45''8776'_270 ∷ T_IsPreorder_76 → T_Σ_14 → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → AgdaAny → T__IsRelatedTo__78 Source #

d_step'45''8776''45''10216'_272 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → AgdaAny → T__IsRelatedTo__78 Source #

du_step'45''8776''45''10216'_272 ∷ T_IsPreorder_76 → T_Σ_14 → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → AgdaAny → T__IsRelatedTo__78 Source #

d_step'45''8776''45''10217'_274 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → AgdaAny → T__IsRelatedTo__78 Source #

du_step'45''8776''45''10217'_274 ∷ T_IsPreorder_76 → T_Σ_14 → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → AgdaAny → T__IsRelatedTo__78 Source #

d_step'45''8776''728'_276 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → AgdaAny → T__IsRelatedTo__78 Source #

du_step'45''8776''728'_276 ∷ T_IsPreorder_76 → T_Σ_14 → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → AgdaAny → T__IsRelatedTo__78 Source #

d_step'45''8804'_280 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → AgdaAny → T__IsRelatedTo__78 Source #

du_step'45''8804'_280 ∷ T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → AgdaAny → T__IsRelatedTo__78 Source #

d_step'45''60'_284 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → AgdaAny → T__IsRelatedTo__78 Source #

du_step'45''60'_284 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T__IsRelatedTo__78 → AgdaAny → T__IsRelatedTo__78 Source #

d__'8718'_288 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T__IsRelatedTo__78 Source #

du__'8718'_288 ∷ T_IsPreorder_76 → AgdaAny → T__IsRelatedTo__78 Source #