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.Algorithmic.Properties 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.Algorithmic
  import qualified MAlonzo.Code.Type.BetaNormal
  import qualified MAlonzo.Code.Utils
  
  -- Algorithmic.Properties.lem-·⋆
  d_lem'45''183''8902'_28 ::
    MAlonzo.Code.Utils.T_Kind_652 ->
    MAlonzo.Code.Utils.T_Kind_652 ->
    MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
    MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
    MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
    MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
    MAlonzo.Code.Algorithmic.T__'8866'__178 ->
    MAlonzo.Code.Algorithmic.T__'8866'__178 ->
    MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_lem'45''183''8902'_28 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9
                          ~v10 ~v11
    = du_lem'45''183''8902'_28
  du_lem'45''183''8902'_28 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_lem'45''183''8902'_28
    = coe
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased
        (coe
           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased
           (coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased erased))
  -- Algorithmic.Properties.lem-unwrap
  d_lem'45'unwrap_54 ::
    MAlonzo.Code.Utils.T_Kind_652 ->
    MAlonzo.Code.Utils.T_Kind_652 ->
    MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
    MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
    MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
    MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
    MAlonzo.Code.Algorithmic.T__'8866'__178 ->
    MAlonzo.Code.Algorithmic.T__'8866'__178 ->
    MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_lem'45'unwrap_54 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 ~v10
                     ~v11
    = du_lem'45'unwrap_54
  du_lem'45'unwrap_54 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_lem'45'unwrap_54
    = coe
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased
        (coe
           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased
           (coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased erased))
  