content: {-# 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.Data.Vec.Relation.Binary.Equality.Cast where
  
  import Data.Text qualified
  import MAlonzo.Code.Agda.Builtin.Equality qualified
  import MAlonzo.Code.Agda.Primitive qualified
  import MAlonzo.Code.Data.Vec.Base qualified
  import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
                      mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
                      word64ToNat)
  import MAlonzo.RTE qualified
  
  -- Data.Vec.Relation.Binary.Equality.Cast.cast-is-id
  d_cast'45'is'45'id_34 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_cast'45'is'45'id_34 = erased
  -- Data.Vec.Relation.Binary.Equality.Cast.cast-trans
  d_cast'45'trans_52 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    Integer ->
    Integer ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_cast'45'trans_52 = erased
  -- Data.Vec.Relation.Binary.Equality.Cast._≈[_]_
  d__'8776''91'_'93'__74 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    Integer ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 -> ()
  d__'8776''91'_'93'__74 = erased
  -- Data.Vec.Relation.Binary.Equality.Cast.≈-reflexive
  d_'8776''45'reflexive_88 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8776''45'reflexive_88 = erased
  -- Data.Vec.Relation.Binary.Equality.Cast.≈-sym
  d_'8776''45'sym_104 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    Integer ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8776''45'sym_104 = erased
  -- Data.Vec.Relation.Binary.Equality.Cast.≈-trans
  d_'8776''45'trans_134 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    Integer ->
    Integer ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8776''45'trans_134 = erased
  -- Data.Vec.Relation.Binary.Equality.Cast.CastReasoning.begin_
  d_begin__162 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    Integer ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_begin__162 = erased
  -- Data.Vec.Relation.Binary.Equality.Cast.CastReasoning._∎
  d__'8718'_168 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d__'8718'_168 = erased
  -- Data.Vec.Relation.Binary.Equality.Cast.CastReasoning._≈⟨⟩_
  d__'8776''10216''10217'__178 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    Integer ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d__'8776''10216''10217'__178 = erased
  -- Data.Vec.Relation.Binary.Equality.Cast.CastReasoning.step-≈-⟩
  d_step'45''8776''45''10217'_194 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    Integer ->
    Integer ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_step'45''8776''45''10217'_194 = erased
  -- Data.Vec.Relation.Binary.Equality.Cast.CastReasoning.step-≈-⟨
  d_step'45''8776''45''10216'_212 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    Integer ->
    Integer ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_step'45''8776''45''10216'_212 = erased
  -- Data.Vec.Relation.Binary.Equality.Cast.CastReasoning.step-≃-⟩
  d_step'45''8771''45''10217'_228 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    Integer ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_step'45''8771''45''10217'_228 = erased
  -- Data.Vec.Relation.Binary.Equality.Cast.CastReasoning.step-≃-⟨
  d_step'45''8771''45''10216'_244 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    Integer ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_step'45''8771''45''10216'_244 = erased
  -- Data.Vec.Relation.Binary.Equality.Cast.CastReasoning.step-≂-⟩
  d_step'45''8770''45''10217'_260 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    Integer ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_step'45''8770''45''10217'_260 = erased
  -- Data.Vec.Relation.Binary.Equality.Cast.CastReasoning.step-≂-⟨
  d_step'45''8770''45''10216'_276 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    Integer ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_step'45''8770''45''10216'_276 = erased
  -- Data.Vec.Relation.Binary.Equality.Cast.CastReasoning.≈-cong
  d_'8776''45'cong_296 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    Integer ->
    Integer ->
    Integer ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    (MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
     MAlonzo.Code.Data.Vec.Base.T_Vec_28) ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8776''45'cong_296 = erased
  