{-# 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.Function.Related 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.Product
import qualified MAlonzo.Code.Function.Base
import qualified MAlonzo.Code.Function.Bijection
import qualified MAlonzo.Code.Function.Bundles
import qualified MAlonzo.Code.Function.Equality
import qualified MAlonzo.Code.Function.Equivalence
import qualified MAlonzo.Code.Function.Injection
import qualified MAlonzo.Code.Function.Inverse
import qualified MAlonzo.Code.Function.LeftInverse
import qualified MAlonzo.Code.Function.Related.Propositional
import qualified MAlonzo.Code.Function.Surjection
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
import qualified MAlonzo.Code.Relation.Binary.Structures
d__'8592'__20 a0 a1 a2 a3 = ()
newtype T__'8592'__20 = C_lam_34 (AgdaAny -> AgdaAny)
d_app'45''8592'_32 :: T__'8592'__20 -> AgdaAny -> AgdaAny
d_app'45''8592'_32 v0
= case coe v0 of
C_lam_34 v1 -> coe v1
_ -> MAlonzo.RTE.mazUnreachableError
d__'8610'__44 a0 a1 a2 a3 = ()
newtype T__'8610'__44
= C_lam_58 MAlonzo.Code.Function.Injection.T_Injection_88
d_app'45''8610'_56 ::
T__'8610'__44 -> MAlonzo.Code.Function.Injection.T_Injection_88
d_app'45''8610'_56 v0
= case coe v0 of
C_lam_58 v1 -> coe v1
_ -> MAlonzo.RTE.mazUnreachableError
d__'8764''91'_'93'__64 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 -> () -> ()
d__'8764''91'_'93'__64 = erased
d_toRelated_100 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
AgdaAny -> AgdaAny
d_toRelated_100 ~v0 ~v1 ~v2 ~v3 v4 v5 = du_toRelated_100 v4 v5
du_toRelated_100 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
AgdaAny -> AgdaAny
du_toRelated_100 v0 v1
= case coe v0 of
MAlonzo.Code.Function.Related.Propositional.C_implication_8
-> coe MAlonzo.Code.Function.Bundles.d_f_648 (coe v1)
MAlonzo.Code.Function.Related.Propositional.C_reverseImplication_10
-> coe
C_lam_34 (coe MAlonzo.Code.Function.Bundles.d_f_648 (coe v1))
MAlonzo.Code.Function.Related.Propositional.C_equivalence_12
-> coe
MAlonzo.Code.Function.Equivalence.du_equivalence_56
(coe MAlonzo.Code.Function.Bundles.d_f_938 (coe v1))
(coe MAlonzo.Code.Function.Bundles.d_g_940 (coe v1))
MAlonzo.Code.Function.Related.Propositional.C_injection_14
-> coe
MAlonzo.Code.Function.Injection.du_injection_140
(coe MAlonzo.Code.Function.Bundles.d_f_712 (coe v1)) erased
MAlonzo.Code.Function.Related.Propositional.C_reverseInjection_16
-> coe
C_lam_58
(coe
MAlonzo.Code.Function.Injection.du_injection_140
(coe MAlonzo.Code.Function.Bundles.d_f_712 (coe v1)) erased)
MAlonzo.Code.Function.Related.Propositional.C_leftInverse_18
-> coe
MAlonzo.Code.Function.LeftInverse.du_leftInverse_242
(coe MAlonzo.Code.Function.Bundles.d_f_1036 (coe v1))
(coe MAlonzo.Code.Function.Bundles.d_g_1038 (coe v1)) erased
MAlonzo.Code.Function.Related.Propositional.C_surjection_20
-> let v2
= MAlonzo.Code.Function.Bundles.d_surjective_786 (coe v1) in
coe
MAlonzo.Code.Function.Surjection.du_surjection_154
(coe MAlonzo.Code.Function.Bundles.d_f_782 (coe v1))
(coe
(\ v3 -> MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (coe v2 v3)))
erased
MAlonzo.Code.Function.Related.Propositional.C_bijection_22
-> let v2
= MAlonzo.Code.Function.Bundles.d_bijective_856 (coe v1) in
case coe v2 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v3 v4
-> coe
MAlonzo.Code.Function.Inverse.du_inverse_156
(coe MAlonzo.Code.Function.Bundles.d_f_852 (coe v1))
(coe
(\ v5 -> MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (coe v4 v5)))
erased erased
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_fromRelated_138 ::
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
AgdaAny -> AgdaAny
d_fromRelated_138 ~v0 ~v1 ~v2 ~v3 v4 v5 = du_fromRelated_138 v4 v5
du_fromRelated_138 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
AgdaAny -> AgdaAny
du_fromRelated_138 v0 v1
= case coe v0 of
MAlonzo.Code.Function.Related.Propositional.C_implication_8
-> coe MAlonzo.Code.Function.Bundles.du_mk'10230'_1290 (coe v1)
MAlonzo.Code.Function.Related.Propositional.C_reverseImplication_10
-> coe
MAlonzo.Code.Function.Bundles.du_mk'10230'_1290
(coe d_app'45''8592'_32 (coe v1))
MAlonzo.Code.Function.Related.Propositional.C_equivalence_12
-> case coe v1 of
MAlonzo.Code.Function.Equivalence.C_Equivalence'46'constructor_269 v2 v3
-> coe
MAlonzo.Code.Function.Bundles.du_mk'8660'_1322
(coe
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38 (coe v2))
(coe
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38 (coe v3))
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Function.Related.Propositional.C_injection_14
-> coe
MAlonzo.Code.Function.Bundles.du_mk'8611'_1296
(coe
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
(coe MAlonzo.Code.Function.Injection.d_to_106 (coe v1)))
erased
MAlonzo.Code.Function.Related.Propositional.C_reverseInjection_16
-> case coe v1 of
C_lam_58 v2
-> coe
MAlonzo.Code.Function.Bundles.du_mk'8611'_1296
(coe
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
(coe MAlonzo.Code.Function.Injection.d_to_106 (coe v2)))
erased
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Function.Related.Propositional.C_leftInverse_18
-> case coe v1 of
MAlonzo.Code.Function.LeftInverse.C_LeftInverse'46'constructor_3301 v2 v3 v4
-> coe
MAlonzo.Code.Function.Bundles.du_mk'8618'_1344
(coe
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38 (coe v2))
(coe
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38 (coe v3))
erased
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Function.Related.Propositional.C_surjection_20
-> case coe v1 of
MAlonzo.Code.Function.Surjection.C_Surjection'46'constructor_1733 v2 v3
-> case coe v3 of
MAlonzo.Code.Function.Surjection.C_Surjective'46'constructor_867 v4 v5
-> coe
MAlonzo.Code.Function.Bundles.du_mk'8608'_1304
(coe
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38 (coe v2))
(coe
MAlonzo.Code.Data.Product.du_'60'_'44'_'62'_132
(coe
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38 (coe v4))
(coe v5))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Function.Related.Propositional.C_bijection_22
-> case coe v1 of
MAlonzo.Code.Function.Inverse.C_Inverse'46'constructor_2615 v2 v3 v4
-> case coe v4 of
MAlonzo.Code.Function.Inverse.C__InverseOf_'46'constructor_1525 v5 v6
-> coe
MAlonzo.Code.Function.Bundles.du_mk'10518'_1312
(coe
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38 (coe v2))
(coe
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased
(coe
MAlonzo.Code.Data.Product.du_'60'_'44'_'62'_132
(coe
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
(coe v3))
(coe v6)))
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
_ -> MAlonzo.RTE.mazUnreachableError
d_Related_220 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 -> () -> () -> ()
d_Related_220 = erased
d_'8596''8658'_238 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() -> () -> MAlonzo.Code.Function.Inverse.T_Inverse_58 -> AgdaAny
d_'8596''8658'_238 v0 ~v1 ~v2 ~v3 ~v4 = du_'8596''8658'_238 v0
du_'8596''8658'_238 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 -> AgdaAny
du_'8596''8658'_238 v0
= case coe v0 of
MAlonzo.Code.Function.Related.Propositional.C_implication_8
-> coe
(\ v1 ->
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
(coe MAlonzo.Code.Function.Inverse.d_to_78 (coe v1)))
MAlonzo.Code.Function.Related.Propositional.C_reverseImplication_10
-> coe
MAlonzo.Code.Function.Base.du__'8728''8242'__216 (coe C_lam_34)
(coe
(\ v1 ->
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
(coe MAlonzo.Code.Function.Inverse.d_from_80 (coe v1))))
MAlonzo.Code.Function.Related.Propositional.C_equivalence_12
-> coe
(\ v1 ->
let v2
= coe
MAlonzo.Code.Function.Inverse.du_bijection_98
(coe
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_404)
(coe v1) in
coe
MAlonzo.Code.Function.Surjection.du_equivalence_92
(coe MAlonzo.Code.Function.Bijection.du_surjection_100 (coe v2)))
MAlonzo.Code.Function.Related.Propositional.C_injection_14
-> coe
(\ v1 ->
coe
MAlonzo.Code.Function.LeftInverse.du_injection_184
(coe
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_404)
(coe MAlonzo.Code.Function.Inverse.du_left'45'inverse_90 (coe v1)))
MAlonzo.Code.Function.Related.Propositional.C_reverseInjection_16
-> coe
MAlonzo.Code.Function.Base.du__'8728''8242'__216 (coe C_lam_58)
(coe
(\ v1 ->
coe
MAlonzo.Code.Function.LeftInverse.du_injection_184
(coe
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_404)
(coe
MAlonzo.Code.Function.Inverse.du_left'45'inverse_90
(coe MAlonzo.Code.Function.Inverse.du_sym_226 (coe v1)))))
MAlonzo.Code.Function.Related.Propositional.C_leftInverse_18
-> coe MAlonzo.Code.Function.Inverse.du_left'45'inverse_90
MAlonzo.Code.Function.Related.Propositional.C_surjection_20
-> coe
(\ v1 ->
coe
MAlonzo.Code.Function.Bijection.du_surjection_100
(coe
MAlonzo.Code.Function.Inverse.du_bijection_98
(coe
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_404)
(coe v1)))
MAlonzo.Code.Function.Related.Propositional.C_bijection_22
-> coe (\ v1 -> v1)
_ -> MAlonzo.RTE.mazUnreachableError
d_'8801''8658'_248 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_'8801''8658'_248 v0 ~v1 ~v2 ~v3 ~v4 = du_'8801''8658'_248 v0
du_'8801''8658'_248 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 -> AgdaAny
du_'8801''8658'_248 v0
= coe
du_'8596''8658'_238 v0
(coe
MAlonzo.Code.Function.Inverse.du_id_186
(coe
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_404))
d_Symmetric'45'kind_250 = ()
data T_Symmetric'45'kind_250 = C_equivalence_252 | C_bijection_254
d_'8970'_'8971'_256 ::
T_Symmetric'45'kind_250 ->
MAlonzo.Code.Function.Related.Propositional.T_Kind_6
d_'8970'_'8971'_256 v0
= case coe v0 of
C_equivalence_252
-> coe MAlonzo.Code.Function.Related.Propositional.C_equivalence_12
C_bijection_254
-> coe MAlonzo.Code.Function.Related.Propositional.C_bijection_22
_ -> MAlonzo.RTE.mazUnreachableError
d_Forward'45'kind_258 = ()
data T_Forward'45'kind_258
= C_implication_260 | C_equivalence_262 | C_injection_264 |
C_left'45'inverse_266 | C_surjection_268 | C_bijection_270
d_'8970'_'8971''8594'_272 ::
T_Forward'45'kind_258 ->
MAlonzo.Code.Function.Related.Propositional.T_Kind_6
d_'8970'_'8971''8594'_272 v0
= case coe v0 of
C_implication_260
-> coe MAlonzo.Code.Function.Related.Propositional.C_implication_8
C_equivalence_262
-> coe MAlonzo.Code.Function.Related.Propositional.C_equivalence_12
C_injection_264
-> coe MAlonzo.Code.Function.Related.Propositional.C_injection_14
C_left'45'inverse_266
-> coe MAlonzo.Code.Function.Related.Propositional.C_leftInverse_18
C_surjection_268
-> coe MAlonzo.Code.Function.Related.Propositional.C_surjection_20
C_bijection_270
-> coe MAlonzo.Code.Function.Related.Propositional.C_bijection_22
_ -> MAlonzo.RTE.mazUnreachableError
d_'8658''8594'_284 ::
T_Forward'45'kind_258 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() -> () -> AgdaAny -> AgdaAny -> AgdaAny
d_'8658''8594'_284 v0 ~v1 ~v2 ~v3 ~v4 = du_'8658''8594'_284 v0
du_'8658''8594'_284 ::
T_Forward'45'kind_258 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8658''8594'_284 v0
= case coe v0 of
C_implication_260 -> coe (\ v1 -> v1)
C_equivalence_262
-> coe
(\ v1 ->
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
(coe MAlonzo.Code.Function.Equivalence.d_to_34 (coe v1)))
C_injection_264
-> coe
(\ v1 ->
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
(coe MAlonzo.Code.Function.Injection.d_to_106 (coe v1)))
C_left'45'inverse_266
-> coe
(\ v1 ->
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
(coe MAlonzo.Code.Function.LeftInverse.d_to_102 (coe v1)))
C_surjection_268
-> coe
(\ v1 ->
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
(coe MAlonzo.Code.Function.Surjection.d_to_72 (coe v1)))
C_bijection_270
-> coe
(\ v1 ->
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
(coe MAlonzo.Code.Function.Inverse.d_to_78 (coe v1)))
_ -> MAlonzo.RTE.mazUnreachableError
d_Backward'45'kind_286 = ()
data T_Backward'45'kind_286
= C_reverse'45'implication_288 | C_equivalence_290 |
C_reverse'45'injection_292 | C_left'45'inverse_294 |
C_surjection_296 | C_bijection_298
d_'8970'_'8971''8592'_300 ::
T_Backward'45'kind_286 ->
MAlonzo.Code.Function.Related.Propositional.T_Kind_6
d_'8970'_'8971''8592'_300 v0
= case coe v0 of
C_reverse'45'implication_288
-> coe
MAlonzo.Code.Function.Related.Propositional.C_reverseImplication_10
C_equivalence_290
-> coe MAlonzo.Code.Function.Related.Propositional.C_equivalence_12
C_reverse'45'injection_292
-> coe
MAlonzo.Code.Function.Related.Propositional.C_reverseInjection_16
C_left'45'inverse_294
-> coe MAlonzo.Code.Function.Related.Propositional.C_leftInverse_18
C_surjection_296
-> coe MAlonzo.Code.Function.Related.Propositional.C_surjection_20
C_bijection_298
-> coe MAlonzo.Code.Function.Related.Propositional.C_bijection_22
_ -> MAlonzo.RTE.mazUnreachableError
d_'8658''8592'_312 ::
T_Backward'45'kind_286 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() -> () -> AgdaAny -> AgdaAny -> AgdaAny
d_'8658''8592'_312 v0 ~v1 ~v2 ~v3 ~v4 = du_'8658''8592'_312 v0
du_'8658''8592'_312 ::
T_Backward'45'kind_286 -> AgdaAny -> AgdaAny -> AgdaAny
du_'8658''8592'_312 v0
= case coe v0 of
C_reverse'45'implication_288 -> coe d_app'45''8592'_32
C_equivalence_290
-> coe
(\ v1 ->
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
(coe MAlonzo.Code.Function.Equivalence.d_from_36 (coe v1)))
C_reverse'45'injection_292
-> coe
(\ v1 ->
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
(coe
MAlonzo.Code.Function.Injection.d_to_106
(coe d_app'45''8610'_56 (coe v1))))
C_left'45'inverse_294
-> coe
(\ v1 ->
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
(coe MAlonzo.Code.Function.LeftInverse.d_from_104 (coe v1)))
C_surjection_296
-> coe
(\ v1 ->
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
(coe
MAlonzo.Code.Function.Surjection.d_from_38
(coe MAlonzo.Code.Function.Surjection.d_surjective_74 (coe v1))))
C_bijection_298
-> coe
(\ v1 ->
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
(coe MAlonzo.Code.Function.Inverse.d_from_80 (coe v1)))
_ -> MAlonzo.RTE.mazUnreachableError
d_Equivalence'45'kind_314 = ()
data T_Equivalence'45'kind_314
= C_equivalence_316 | C_left'45'inverse_318 | C_surjection_320 |
C_bijection_322
d_'8970'_'8971''8660'_324 ::
T_Equivalence'45'kind_314 ->
MAlonzo.Code.Function.Related.Propositional.T_Kind_6
d_'8970'_'8971''8660'_324 v0
= case coe v0 of
C_equivalence_316
-> coe MAlonzo.Code.Function.Related.Propositional.C_equivalence_12
C_left'45'inverse_318
-> coe MAlonzo.Code.Function.Related.Propositional.C_leftInverse_18
C_surjection_320
-> coe MAlonzo.Code.Function.Related.Propositional.C_surjection_20
C_bijection_322
-> coe MAlonzo.Code.Function.Related.Propositional.C_bijection_22
_ -> MAlonzo.RTE.mazUnreachableError
d_'8658''8660'_336 ::
T_Equivalence'45'kind_314 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() -> AgdaAny -> MAlonzo.Code.Function.Equivalence.T_Equivalence_16
d_'8658''8660'_336 v0 ~v1 ~v2 ~v3 ~v4 = du_'8658''8660'_336 v0
du_'8658''8660'_336 ::
T_Equivalence'45'kind_314 ->
AgdaAny -> MAlonzo.Code.Function.Equivalence.T_Equivalence_16
du_'8658''8660'_336 v0
= case coe v0 of
C_equivalence_316 -> coe (\ v1 -> v1)
C_left'45'inverse_318
-> coe MAlonzo.Code.Function.LeftInverse.du_equivalence_186
C_surjection_320
-> coe MAlonzo.Code.Function.Surjection.du_equivalence_92
C_bijection_322
-> coe
(\ v1 ->
let v2
= coe
MAlonzo.Code.Function.Inverse.du_bijection_98
(coe
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_404)
(coe v1) in
coe
MAlonzo.Code.Function.Surjection.du_equivalence_92
(coe MAlonzo.Code.Function.Bijection.du_surjection_100 (coe v2)))
_ -> MAlonzo.RTE.mazUnreachableError
d_'8660''8970'_'8971'_338 ::
T_Symmetric'45'kind_250 -> T_Equivalence'45'kind_314
d_'8660''8970'_'8971'_338 v0
= case coe v0 of
C_equivalence_252 -> coe C_equivalence_316
C_bijection_254 -> coe C_bijection_322
_ -> MAlonzo.RTE.mazUnreachableError
d_'8594''8970'_'8971'_340 ::
T_Equivalence'45'kind_314 -> T_Forward'45'kind_258
d_'8594''8970'_'8971'_340 v0
= case coe v0 of
C_equivalence_316 -> coe C_equivalence_262
C_left'45'inverse_318 -> coe C_left'45'inverse_266
C_surjection_320 -> coe C_surjection_268
C_bijection_322 -> coe C_bijection_270
_ -> MAlonzo.RTE.mazUnreachableError
d_'8592''8970'_'8971'_342 ::
T_Equivalence'45'kind_314 -> T_Backward'45'kind_286
d_'8592''8970'_'8971'_342 v0
= case coe v0 of
C_equivalence_316 -> coe C_equivalence_290
C_left'45'inverse_318 -> coe C_left'45'inverse_294
C_surjection_320 -> coe C_surjection_296
C_bijection_322 -> coe C_bijection_298
_ -> MAlonzo.RTE.mazUnreachableError
d__op_344 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
MAlonzo.Code.Function.Related.Propositional.T_Kind_6
d__op_344 v0
= case coe v0 of
MAlonzo.Code.Function.Related.Propositional.C_implication_8
-> coe
MAlonzo.Code.Function.Related.Propositional.C_reverseImplication_10
MAlonzo.Code.Function.Related.Propositional.C_reverseImplication_10
-> coe MAlonzo.Code.Function.Related.Propositional.C_implication_8
MAlonzo.Code.Function.Related.Propositional.C_equivalence_12
-> coe v0
MAlonzo.Code.Function.Related.Propositional.C_injection_14
-> coe
MAlonzo.Code.Function.Related.Propositional.C_reverseInjection_16
MAlonzo.Code.Function.Related.Propositional.C_reverseInjection_16
-> coe MAlonzo.Code.Function.Related.Propositional.C_injection_14
MAlonzo.Code.Function.Related.Propositional.C_leftInverse_18
-> coe MAlonzo.Code.Function.Related.Propositional.C_surjection_20
MAlonzo.Code.Function.Related.Propositional.C_surjection_20
-> coe MAlonzo.Code.Function.Related.Propositional.C_leftInverse_18
MAlonzo.Code.Function.Related.Propositional.C_bijection_22
-> coe v0
_ -> MAlonzo.RTE.mazUnreachableError
d_reverse_356 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() -> () -> AgdaAny -> AgdaAny
d_reverse_356 v0 ~v1 ~v2 ~v3 ~v4 = du_reverse_356 v0
du_reverse_356 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
AgdaAny -> AgdaAny
du_reverse_356 v0
= case coe v0 of
MAlonzo.Code.Function.Related.Propositional.C_implication_8
-> coe C_lam_34
MAlonzo.Code.Function.Related.Propositional.C_reverseImplication_10
-> coe d_app'45''8592'_32
MAlonzo.Code.Function.Related.Propositional.C_equivalence_12
-> coe MAlonzo.Code.Function.Equivalence.du_sym_100
MAlonzo.Code.Function.Related.Propositional.C_injection_14
-> coe C_lam_58
MAlonzo.Code.Function.Related.Propositional.C_reverseInjection_16
-> coe d_app'45''8610'_56
MAlonzo.Code.Function.Related.Propositional.C_leftInverse_18
-> coe MAlonzo.Code.Function.Surjection.du_fromRightInverse_106
MAlonzo.Code.Function.Related.Propositional.C_surjection_20
-> coe MAlonzo.Code.Function.Surjection.du_right'45'inverse_82
MAlonzo.Code.Function.Related.Propositional.C_bijection_22
-> coe MAlonzo.Code.Function.Inverse.du_sym_226
_ -> MAlonzo.RTE.mazUnreachableError
d_K'45'refl_362 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 -> () -> AgdaAny
d_K'45'refl_362 v0 ~v1 ~v2 = du_K'45'refl_362 v0
du_K'45'refl_362 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 -> AgdaAny
du_K'45'refl_362 v0
= case coe v0 of
MAlonzo.Code.Function.Related.Propositional.C_implication_8
-> coe (\ v1 -> v1)
MAlonzo.Code.Function.Related.Propositional.C_reverseImplication_10
-> coe C_lam_34 (coe (\ v1 -> v1))
MAlonzo.Code.Function.Related.Propositional.C_equivalence_12
-> coe MAlonzo.Code.Function.Equivalence.du_id_66
MAlonzo.Code.Function.Related.Propositional.C_injection_14
-> coe MAlonzo.Code.Function.Injection.du_id_152
MAlonzo.Code.Function.Related.Propositional.C_reverseInjection_16
-> coe C_lam_58 (coe MAlonzo.Code.Function.Injection.du_id_152)
MAlonzo.Code.Function.Related.Propositional.C_leftInverse_18
-> coe
MAlonzo.Code.Function.LeftInverse.du_id_256
(coe
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_404)
MAlonzo.Code.Function.Related.Propositional.C_surjection_20
-> coe
MAlonzo.Code.Function.Surjection.du_id_168
(coe
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_404)
MAlonzo.Code.Function.Related.Propositional.C_bijection_22
-> coe
MAlonzo.Code.Function.Inverse.du_id_186
(coe
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_404)
_ -> MAlonzo.RTE.mazUnreachableError
d_K'45'reflexive_368 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_K'45'reflexive_368 v0 ~v1 ~v2 ~v3 ~v4 = du_K'45'reflexive_368 v0
du_K'45'reflexive_368 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 -> AgdaAny
du_K'45'reflexive_368 v0 = coe du_K'45'refl_362 (coe v0)
d_K'45'trans_378 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
d_K'45'trans_378 v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 = du_K'45'trans_378 v0
du_K'45'trans_378 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
AgdaAny -> AgdaAny -> AgdaAny
du_K'45'trans_378 v0
= case coe v0 of
MAlonzo.Code.Function.Related.Propositional.C_implication_8
-> coe
(\ v1 v2 ->
coe
MAlonzo.Code.Function.Base.du__'8728''8242'__216 (coe v2) (coe v1))
MAlonzo.Code.Function.Related.Propositional.C_reverseImplication_10
-> coe
(\ v1 v2 ->
coe
C_lam_34
(coe
(\ v3 ->
coe d_app'45''8592'_32 v1 (coe d_app'45''8592'_32 v2 v3))))
MAlonzo.Code.Function.Related.Propositional.C_equivalence_12
-> coe
(\ v1 v2 ->
coe
MAlonzo.Code.Function.Equivalence.du__'8728'__82 (coe v2) (coe v1))
MAlonzo.Code.Function.Related.Propositional.C_injection_14
-> coe
(\ v1 v2 ->
coe
MAlonzo.Code.Function.Injection.du__'8728'__172 (coe v2) (coe v1))
MAlonzo.Code.Function.Related.Propositional.C_reverseInjection_16
-> coe
(\ v1 v2 ->
coe
C_lam_58
(coe
MAlonzo.Code.Function.Injection.du__'8728'__172
(coe d_app'45''8610'_56 (coe v1))
(coe d_app'45''8610'_56 (coe v2))))
MAlonzo.Code.Function.Related.Propositional.C_leftInverse_18
-> coe
(\ v1 v2 ->
coe
MAlonzo.Code.Function.LeftInverse.du__'8728'__280
(coe
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_404)
(coe v2) (coe v1))
MAlonzo.Code.Function.Related.Propositional.C_surjection_20
-> coe
(\ v1 v2 ->
coe
MAlonzo.Code.Function.Surjection.du__'8728'__196
(coe
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_404)
(coe v2) (coe v1))
MAlonzo.Code.Function.Related.Propositional.C_bijection_22
-> coe
(\ v1 v2 ->
coe
MAlonzo.Code.Function.Inverse.du__'8728'__208
(coe
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_404)
(coe
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_404)
(coe v2) (coe v1))
_ -> MAlonzo.RTE.mazUnreachableError
d_SK'45'sym_394 ::
T_Symmetric'45'kind_250 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() -> () -> AgdaAny -> AgdaAny
d_SK'45'sym_394 v0 ~v1 ~v2 ~v3 ~v4 = du_SK'45'sym_394 v0
du_SK'45'sym_394 :: T_Symmetric'45'kind_250 -> AgdaAny -> AgdaAny
du_SK'45'sym_394 v0
= case coe v0 of
C_equivalence_252
-> coe MAlonzo.Code.Function.Equivalence.du_sym_100
C_bijection_254 -> coe MAlonzo.Code.Function.Inverse.du_sym_226
_ -> MAlonzo.RTE.mazUnreachableError
d_SK'45'isEquivalence_400 ::
T_Symmetric'45'kind_250 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_SK'45'isEquivalence_400 v0 ~v1 = du_SK'45'isEquivalence_400 v0
du_SK'45'isEquivalence_400 ::
T_Symmetric'45'kind_250 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
du_SK'45'isEquivalence_400 v0
= coe
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_519
(\ v1 -> coe du_K'45'refl_362 (coe d_'8970'_'8971'_256 (coe v0)))
(\ v1 v2 -> coe du_SK'45'sym_394 (coe v0))
(\ v1 v2 v3 ->
coe du_K'45'trans_378 (coe d_'8970'_'8971'_256 (coe v0)))
d_SK'45'setoid_408 ::
T_Symmetric'45'kind_250 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_SK'45'setoid_408 v0 ~v1 = du_SK'45'setoid_408 v0
du_SK'45'setoid_408 ::
T_Symmetric'45'kind_250 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du_SK'45'setoid_408 v0
= coe
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_575
(coe du_SK'45'isEquivalence_400 (coe v0))
d_K'45'isPreorder_418 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_K'45'isPreorder_418 v0 ~v1 = du_K'45'isPreorder_418 v0
du_K'45'isPreorder_418 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
du_K'45'isPreorder_418 v0
= coe
MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_2409
(coe du_SK'45'isEquivalence_400 (coe C_bijection_254))
(\ v1 v2 -> coe du_'8596''8658'_238 (coe v0))
(\ v1 v2 v3 -> coe du_K'45'trans_378 (coe v0))
d_K'45'preorder_426 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_K'45'preorder_426 v0 ~v1 = du_K'45'preorder_426 v0
du_K'45'preorder_426 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_K'45'preorder_426 v0
= coe
MAlonzo.Code.Relation.Binary.Bundles.C_Preorder'46'constructor_1855
(coe du_K'45'isPreorder_418 (coe v0))
d__'8764''10216'_'10217'__448 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
d__'8764''10216'_'10217'__448 v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 v7 v8
= du__'8764''10216'_'10217'__448 v0 v7 v8
du__'8764''10216'_'10217'__448 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
AgdaAny -> AgdaAny -> AgdaAny
du__'8764''10216'_'10217'__448 v0 v1 v2
= coe du_K'45'trans_378 v0 v1 v2
d__'8596''10216'_'10217'__468 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
() ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 -> AgdaAny -> AgdaAny
d__'8596''10216'_'10217'__468 v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 v7 v8
= du__'8596''10216'_'10217'__468 v0 v7 v8
du__'8596''10216'_'10217'__468 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
MAlonzo.Code.Function.Inverse.T_Inverse_58 -> AgdaAny -> AgdaAny
du__'8596''10216'_'10217'__468 v0 v1 v2
= coe
du__'8764''10216'_'10217'__448 (coe v0)
(coe du_'8596''8658'_238 v0 v1) (coe v2)
d__'8596''10216''10217'__486 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() -> () -> AgdaAny -> AgdaAny
d__'8596''10216''10217'__486 ~v0 ~v1 ~v2 ~v3 ~v4 v5
= du__'8596''10216''10217'__486 v5
du__'8596''10216''10217'__486 :: AgdaAny -> AgdaAny
du__'8596''10216''10217'__486 v0 = coe v0
d__'8801''10216'_'10217'__504 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
() ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
AgdaAny -> AgdaAny
d__'8801''10216'_'10217'__504 v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 v7
= du__'8801''10216'_'10217'__504 v0 v7
du__'8801''10216'_'10217'__504 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
AgdaAny -> AgdaAny
du__'8801''10216'_'10217'__504 v0 v1
= coe
du__'8764''10216'_'10217'__448 (coe v0)
(coe du_'8801''8658'_248 (coe v0)) (coe v1)
d__'8718'_518 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 -> () -> AgdaAny
d__'8718'_518 v0 ~v1 ~v2 = du__'8718'_518 v0
du__'8718'_518 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 -> AgdaAny
du__'8718'_518 v0 = coe du_K'45'refl_362 (coe v0)
d_InducedRelation'8321'_528 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() -> (AgdaAny -> ()) -> AgdaAny -> AgdaAny -> ()
d_InducedRelation'8321'_528 = erased
d_InducedPreorder'8321'_544 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
(AgdaAny -> ()) ->
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_InducedPreorder'8321'_544 v0 ~v1 ~v2 ~v3 ~v4
= du_InducedPreorder'8321'_544 v0
du_InducedPreorder'8321'_544 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_InducedPreorder'8321'_544 v0
= coe
MAlonzo.Code.Relation.Binary.Bundles.C_Preorder'46'constructor_1855
(coe
MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_2409
(coe
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
(coe
(\ v1 v2 v3 ->
coe
du_'8596''8658'_238 v0
(coe
du_K'45'reflexive_368
(coe MAlonzo.Code.Function.Related.Propositional.C_bijection_22))))
(coe (\ v1 v2 v3 -> coe du_K'45'trans_378 (coe v0))))
d_InducedEquivalence'8321'_608 ::
T_Symmetric'45'kind_250 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
(AgdaAny -> ()) -> MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_InducedEquivalence'8321'_608 v0 ~v1 ~v2 ~v3 ~v4
= du_InducedEquivalence'8321'_608 v0
du_InducedEquivalence'8321'_608 ::
T_Symmetric'45'kind_250 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du_InducedEquivalence'8321'_608 v0
= coe
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_575
(coe
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_519
(coe
(\ v1 -> coe du_K'45'refl_362 (coe d_'8970'_'8971'_256 (coe v0))))
(coe (\ v1 v2 -> coe du_SK'45'sym_394 (coe v0)))
(coe
(\ v1 v2 v3 ->
coe du_K'45'trans_378 (coe d_'8970'_'8971'_256 (coe v0)))))
d_InducedRelation'8322'_624 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> ()
d_InducedRelation'8322'_624 = erased
d_InducedPreorder'8322'_646 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_InducedPreorder'8322'_646 v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6
= du_InducedPreorder'8322'_646 v0
du_InducedPreorder'8322'_646 ::
MAlonzo.Code.Function.Related.Propositional.T_Kind_6 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_InducedPreorder'8322'_646 v0
= coe
MAlonzo.Code.Relation.Binary.Bundles.C_Preorder'46'constructor_1855
(coe
MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_2409
(coe
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
(coe
(\ v1 v2 v3 v4 ->
coe
du_'8596''8658'_238 v0
(coe
du_K'45'reflexive_368
(coe MAlonzo.Code.Function.Related.Propositional.C_bijection_22))))
(coe
(\ v1 v2 v3 v4 v5 v6 ->
coe du_K'45'trans_378 v0 (coe v4 v6) (coe v5 v6))))
d_InducedEquivalence'8322'_722 ::
T_Symmetric'45'kind_250 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
MAlonzo.Code.Agda.Primitive.T_Level_14 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_InducedEquivalence'8322'_722 v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6
= du_InducedEquivalence'8322'_722 v0
du_InducedEquivalence'8322'_722 ::
T_Symmetric'45'kind_250 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
du_InducedEquivalence'8322'_722 v0
= coe
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_575
(coe
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_519
(coe
(\ v1 v2 ->
coe du_K'45'refl_362 (coe d_'8970'_'8971'_256 (coe v0))))
(coe (\ v1 v2 v3 v4 -> coe du_SK'45'sym_394 v0 (coe v3 v4)))
(coe
(\ v1 v2 v3 v4 v5 v6 ->
coe
du_K'45'trans_378 (d_'8970'_'8971'_256 (coe v0)) (coe v4 v6)
(coe v5 v6))))