formal-ledger-specification commit f3593d367bc5891a5e59a5542065134979…

…5172b8

MAlonzo/Code/Axiom/Set.hs

@@ -799,7 +799,7 @@ du_'8712''45'concatMap'738'_502 v0 v1 v2 v3
                      du_'8712''45'unions_422 (coe v0) (coe v2)
                      (coe du_map_380 v0 v3 v1)))
                (coe
-                  MAlonzo.Code.Data.Product.Properties.Ext.du_'8707''45'cong'8242'_46
+                  MAlonzo.Code.Data.Product.Properties.Ext.du_'8707''45'cong'8242'_54
                   (coe MAlonzo.Code.Function.Related.Propositional.C_equivalence_12)
                   (coe
                      (\ v4 ->
@@ -812,7 +812,7 @@ du_'8712''45'concatMap'738'_502 v0 v1 v2 v3
                              (coe
                                 MAlonzo.Code.Function.Related.Propositional.C_equivalence_12))))))
             (coe
-               MAlonzo.Code.Data.Product.Properties.Ext.du_'8707''45'cong'8242'_46
+               MAlonzo.Code.Data.Product.Properties.Ext.du_'8707''45'cong'8242'_54
                (coe MAlonzo.Code.Function.Related.Propositional.C_equivalence_12)
                (coe
                   (\ v4 ->
@@ -861,12 +861,12 @@ du_'8712''45'concatMap'738'_502 v0 v1 v2 v3
          (coe
             MAlonzo.Code.Data.Product.Properties.du_'8707''8707''8596''8707''8707'_250))
       (coe
-         MAlonzo.Code.Data.Product.Properties.Ext.du_'8707''45'cong'8242'_46
+         MAlonzo.Code.Data.Product.Properties.Ext.du_'8707''45'cong'8242'_54
          (coe MAlonzo.Code.Function.Related.Propositional.C_equivalence_12)
          (coe
             (\ v4 ->
                coe
-                 MAlonzo.Code.Data.Product.Properties.Ext.du_'8707''45''8801'_58
+                 MAlonzo.Code.Data.Product.Properties.Ext.du_'8707''45''8801'_66
                  (coe v3 v4))))
 -- Axiom.Set.Theory.mapPartial
 d_mapPartial_558 ::
@@ -924,7 +924,7 @@ du_'8712''45'mapPartial_568 v0 v1 v2 v3
             du_'8712''45'concatMap'738'_502 (coe v0) (coe v1) (coe v2)
             (coe du_partialToSet_454 (coe v0) (coe v3))))
       (coe
-         MAlonzo.Code.Data.Product.Properties.Ext.du_'8707''45'cong'8242'_46
+         MAlonzo.Code.Data.Product.Properties.Ext.du_'8707''45'cong'8242'_54
          (coe MAlonzo.Code.Function.Related.Propositional.C_equivalence_12)
          (coe
             (\ v4 ->

MAlonzo/Code/Axiom/Set/Factor.hs

@@ -56,43 +56,43 @@ d_finite_48 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 -> () -> AgdaAny -> ()
 d_finite_48 = erased
 -- Axiom.Set.Factor._ᶠ
-d__'7584'_284 ::
+d__'7584'_286 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   AgdaAny ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
-d__'7584'_284 ~v0 ~v1 v2 v3 = du__'7584'_284 v2 v3
-du__'7584'_284 ::
+d__'7584'_286 ~v0 ~v1 v2 v3 = du__'7584'_286 v2 v3
+du__'7584'_286 ::
   AgdaAny ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
-du__'7584'_284 v0 v1
+du__'7584'_286 v0 v1
   = coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v0) (coe v1)
 -- Axiom.Set.Factor.∪-preserves-finite'
-d_'8746''45'preserves'45'finite''_294 ::
+d_'8746''45'preserves'45'finite''_296 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
-d_'8746''45'preserves'45'finite''_294 v0 ~v1 v2 v3 v4 v5
-  = du_'8746''45'preserves'45'finite''_294 v0 v2 v3 v4 v5
-du_'8746''45'preserves'45'finite''_294 ::
+d_'8746''45'preserves'45'finite''_296 v0 ~v1 v2 v3 v4 v5
+  = du_'8746''45'preserves'45'finite''_296 v0 v2 v3 v4 v5
+du_'8746''45'preserves'45'finite''_296 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
-du_'8746''45'preserves'45'finite''_294 v0 v1 v2 v3 v4
+du_'8746''45'preserves'45'finite''_296 v0 v1 v2 v3 v4
   = coe
-      MAlonzo.Code.Axiom.Set.Properties.du_'8746''45'preserves'45'finite_586
+      MAlonzo.Code.Axiom.Set.Properties.du_'8746''45'preserves'45'finite_616
       (coe v0) (coe v1) (coe v2) (coe v3) (coe v4)
 -- Axiom.Set.Factor.Factor.factor
-d_factor_316 ::
+d_factor_318 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   () ->
@@ -103,19 +103,19 @@ d_factor_316 ::
    (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714) ->
    AgdaAny) ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
-d_factor_316 ~v0 ~v1 ~v2 ~v3 v4 ~v5 v6 = du_factor_316 v4 v6
-du_factor_316 ::
+d_factor_318 ~v0 ~v1 ~v2 ~v3 v4 ~v5 v6 = du_factor_318 v4 v6
+du_factor_318 ::
   ([AgdaAny] -> AgdaAny) ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
-du_factor_316 v0 v1
+du_factor_318 v0 v1
   = case coe v1 of
       MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v2 v3
         -> case coe v3 of
              MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v4 v5 -> coe v0 v4
              _ -> MAlonzo.RTE.mazUnreachableError
       _ -> MAlonzo.RTE.mazUnreachableError
 -- Axiom.Set.Factor.Factor.factor-cong
-d_factor'45'cong_320 ::
+d_factor'45'cong_322 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   () ->
@@ -128,17 +128,17 @@ d_factor'45'cong_320 ::
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
-d_factor'45'cong_320 ~v0 ~v1 ~v2 ~v3 ~v4 v5 v6 v7 v8
-  = du_factor'45'cong_320 v5 v6 v7 v8
-du_factor'45'cong_320 ::
+d_factor'45'cong_322 ~v0 ~v1 ~v2 ~v3 ~v4 v5 v6 v7 v8
+  = du_factor'45'cong_322 v5 v6 v7 v8
+du_factor'45'cong_322 ::
   ([AgdaAny] ->
    [AgdaAny] ->
    (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714) ->
    AgdaAny) ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
-du_factor'45'cong_320 v0 v1 v2 v3
+du_factor'45'cong_322 v0 v1 v2 v3
   = case coe v1 of
       MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v4 v5
         -> case coe v5 of
@@ -198,7 +198,7 @@ du_factor'45'cong_320 v0 v1 v2 v3
              _ -> MAlonzo.RTE.mazUnreachableError
       _ -> MAlonzo.RTE.mazUnreachableError
 -- Axiom.Set.Factor.Factor.factor-∪
-d_factor'45''8746'_356 ::
+d_factor'45''8746'_358 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   () ->
@@ -214,27 +214,27 @@ d_factor'45''8746'_356 ::
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   ([AgdaAny] -> [AgdaAny] -> AgdaAny) -> AgdaAny
-d_factor'45''8746'_356 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 v7 v8 v9 v10 v11
-  = du_factor'45''8746'_356 v7 v8 v9 v10 v11
-du_factor'45''8746'_356 ::
+d_factor'45''8746'_358 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 v7 v8 v9 v10 v11
+  = du_factor'45''8746'_358 v7 v8 v9 v10 v11
+du_factor'45''8746'_358 ::
   AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   ([AgdaAny] -> [AgdaAny] -> AgdaAny) -> AgdaAny
-du_factor'45''8746'_356 v0 v1 v2 v3 v4
+du_factor'45''8746'_358 v0 v1 v2 v3 v4
   = coe
       v4
       (MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
          (coe
             MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
-            (coe du__'7584'_284 (coe v0) (coe v2))))
+            (coe du__'7584'_286 (coe v0) (coe v2))))
       (MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
          (coe
             MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
-            (coe du__'7584'_284 (coe v1) (coe v3))))
+            (coe du__'7584'_286 (coe v1) (coe v3))))
 -- Axiom.Set.Factor.FactorUnique.f-cong'
-d_f'45'cong''_384 ::
+d_f'45'cong''_386 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   () ->
@@ -249,9 +249,9 @@ d_f'45'cong''_384 ::
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714) ->
   AgdaAny
-d_f'45'cong''_384 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8 v9
-  = du_f'45'cong''_384 v6 v7 v8 v9
-du_f'45'cong''_384 ::
+d_f'45'cong''_386 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8 v9
+  = du_f'45'cong''_386 v6 v7 v8 v9
+du_f'45'cong''_386 ::
   (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Data.List.Relation.Binary.Permutation.Propositional.T__'8621'__16 ->
@@ -260,7 +260,7 @@ du_f'45'cong''_384 ::
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714) ->
   AgdaAny
-du_f'45'cong''_384 v0 v1 v2 v3
+du_f'45'cong''_386 v0 v1 v2 v3
   = coe
       v0 v1 v2
       (coe
@@ -271,7 +271,7 @@ du_f'45'cong''_384 v0 v1 v2 v3
             MAlonzo.Code.Data.List.Relation.Unary.Unique.Propositional.Properties.WithK.du_unique'8743'set'8658'bag_64
             (coe v3)))
 -- Axiom.Set.Factor.FactorUnique.deduplicate-Σ
-d_deduplicate'45'Σ_392 ::
+d_deduplicate'45'Σ_394 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   () ->
@@ -283,12 +283,12 @@ d_deduplicate'45'Σ_392 ::
    MAlonzo.Code.Data.List.Relation.Binary.Permutation.Propositional.T__'8621'__16 ->
    AgdaAny) ->
   [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
-d_deduplicate'45'Σ_392 ~v0 ~v1 ~v2 v3 ~v4 ~v5 ~v6 v7
-  = du_deduplicate'45'Σ_392 v3 v7
-du_deduplicate'45'Σ_392 ::
+d_deduplicate'45'Σ_394 ~v0 ~v1 ~v2 v3 ~v4 ~v5 ~v6 v7
+  = du_deduplicate'45'Σ_394 v3 v7
+du_deduplicate'45'Σ_394 ::
   MAlonzo.Code.Class.DecEq.Core.T_DecEq_10 ->
   [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
-du_deduplicate'45'Σ_392 v0 v1
+du_deduplicate'45'Σ_394 v0 v1
   = coe
       MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
       (coe
@@ -298,7 +298,7 @@ du_deduplicate'45'Σ_392 v0 v1
          MAlonzo.Code.Data.List.Relation.Unary.Unique.DecPropositional.Properties.du_deduplicate'45''33'_42
          (MAlonzo.Code.Class.DecEq.Core.d__'8799'__16 (coe v0)) v1)
 -- Axiom.Set.Factor.FactorUnique.ext
-d_ext_396 ::
+d_ext_398 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   () ->
@@ -310,15 +310,15 @@ d_ext_396 ::
    MAlonzo.Code.Data.List.Relation.Binary.Permutation.Propositional.T__'8621'__16 ->
    AgdaAny) ->
   [AgdaAny] -> AgdaAny
-d_ext_396 ~v0 ~v1 ~v2 v3 ~v4 v5 ~v6 v7 = du_ext_396 v3 v5 v7
-du_ext_396 ::
+d_ext_398 ~v0 ~v1 ~v2 v3 ~v4 v5 ~v6 v7 = du_ext_398 v3 v5 v7
+du_ext_398 ::
   MAlonzo.Code.Class.DecEq.Core.T_DecEq_10 ->
   (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny) ->
   [AgdaAny] -> AgdaAny
-du_ext_396 v0 v1 v2
-  = coe v1 (coe du_deduplicate'45'Σ_392 (coe v0) (coe v2))
+du_ext_398 v0 v1 v2
+  = coe v1 (coe du_deduplicate'45'Σ_394 (coe v0) (coe v2))
 -- Axiom.Set.Factor.FactorUnique.ext-cong
-d_ext'45'cong_402 ::
+d_ext'45'cong_404 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   () ->
@@ -333,9 +333,9 @@ d_ext'45'cong_402 ::
   [AgdaAny] ->
   (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714) ->
   AgdaAny
-d_ext'45'cong_402 ~v0 ~v1 ~v2 v3 ~v4 ~v5 v6 v7 v8 v9
-  = du_ext'45'cong_402 v3 v6 v7 v8 v9
-du_ext'45'cong_402 ::
+d_ext'45'cong_404 ~v0 ~v1 ~v2 v3 ~v4 ~v5 v6 v7 v8 v9
+  = du_ext'45'cong_404 v3 v6 v7 v8 v9
+du_ext'45'cong_404 ::
   MAlonzo.Code.Class.DecEq.Core.T_DecEq_10 ->
   (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
@@ -345,9 +345,9 @@ du_ext'45'cong_402 ::
   [AgdaAny] ->
   (AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714) ->
   AgdaAny
-du_ext'45'cong_402 v0 v1 v2 v3 v4
+du_ext'45'cong_404 v0 v1 v2 v3 v4
   = coe
-      du_f'45'cong''_384 (coe v1)
+      du_f'45'cong''_386 (coe v1)
       (coe
          MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
          (coe
@@ -405,7 +405,7 @@ du_ext'45'cong_402 v0 v1 v2 v3 v4
                     MAlonzo.Code.Data.List.Ext.Properties.du_'8712''45'dedup_178
                     (coe v0) (coe v2) (coe v5)))))
 -- Axiom.Set.Factor.FactorUnique._.factor
-d_factor_418 ::
+d_factor_420 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   () ->
@@ -417,15 +417,15 @@ d_factor_418 ::
    MAlonzo.Code.Data.List.Relation.Binary.Permutation.Propositional.T__'8621'__16 ->
    AgdaAny) ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
-d_factor_418 ~v0 ~v1 ~v2 v3 ~v4 v5 ~v6 = du_factor_418 v3 v5
-du_factor_418 ::
+d_factor_420 ~v0 ~v1 ~v2 v3 ~v4 v5 ~v6 = du_factor_420 v3 v5
+du_factor_420 ::
   MAlonzo.Code.Class.DecEq.Core.T_DecEq_10 ->
   (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny) ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
-du_factor_418 v0 v1
-  = coe du_factor_316 (coe du_ext_396 (coe v0) (coe v1))
+du_factor_420 v0 v1
+  = coe du_factor_318 (coe du_ext_398 (coe v0) (coe v1))
 -- Axiom.Set.Factor.FactorUnique._.factor-cong
-d_factor'45'cong_420 ::
+d_factor'45'cong_422 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   () ->
@@ -439,9 +439,9 @@ d_factor'45'cong_420 ::
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
-d_factor'45'cong_420 ~v0 ~v1 ~v2 v3 ~v4 ~v5 v6
-  = du_factor'45'cong_420 v3 v6
-du_factor'45'cong_420 ::
+d_factor'45'cong_422 ~v0 ~v1 ~v2 v3 ~v4 ~v5 v6
+  = du_factor'45'cong_422 v3 v6
+du_factor'45'cong_422 ::
   MAlonzo.Code.Class.DecEq.Core.T_DecEq_10 ->
   (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
@@ -450,11 +450,11 @@ du_factor'45'cong_420 ::
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny
-du_factor'45'cong_420 v0 v1
+du_factor'45'cong_422 v0 v1
   = coe
-      du_factor'45'cong_320 (coe du_ext'45'cong_402 (coe v0) (coe v1))
+      du_factor'45'cong_322 (coe du_ext'45'cong_404 (coe v0) (coe v1))
 -- Axiom.Set.Factor.FactorUnique._.factor-∪
-d_factor'45''8746'_422 ::
+d_factor'45''8746'_424 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   () ->
@@ -471,19 +471,19 @@ d_factor'45''8746'_422 ::
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   ([AgdaAny] -> [AgdaAny] -> AgdaAny) -> AgdaAny
-d_factor'45''8746'_422 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6
-  = du_factor'45''8746'_422
-du_factor'45''8746'_422 ::
+d_factor'45''8746'_424 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6
+  = du_factor'45''8746'_424
+du_factor'45''8746'_424 ::
   (AgdaAny -> AgdaAny -> AgdaAny -> ()) ->
   AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   ([AgdaAny] -> [AgdaAny] -> AgdaAny) -> AgdaAny
-du_factor'45''8746'_422 v0 v1 v2 v3 v4 v5
-  = coe du_factor'45''8746'_356 v1 v2 v3 v4 v5
+du_factor'45''8746'_424 v0 v1 v2 v3 v4 v5
+  = coe du_factor'45''8746'_358 v1 v2 v3 v4 v5
 -- Axiom.Set.Factor.FactorUnique.factor-∪'
-d_factor'45''8746'''_438 ::
+d_factor'45''8746'''_440 ::
   MAlonzo.Code.Axiom.Set.T_Theory_82 ->
   () ->
   () ->
@@ -509,10 +509,10 @@ d_factor'45''8746'''_438 ::
     MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
    AgdaAny) ->
   AgdaAny
-d_factor'45''8746'''_438 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9
+d_factor'45''8746'''_440 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9
                          v10 v11 ~v12 v13
-  = du_factor'45''8746'''_438 v10 v11 v13
-du_factor'45''8746'''_438 ::
+  = du_factor'45''8746'''_440 v10 v11 v13
+du_factor'45''8746'''_440 ::
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   ([AgdaAny] ->
@@ -522,7 +522,7 @@ du_factor'45''8746'''_438 ::
     MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
    AgdaAny) ->
   AgdaAny
-du_factor'45''8746'''_438 v0 v1 v2
+du_factor'45''8746'''_440 v0 v1 v2
   = case coe v0 of
       MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v3 v4
         -> case coe v1 of