From 0cdbe87262c7ca8dfabd921d9f23323990611d7a Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 3 Apr 2019 15:57:34 +0200
Subject: rename test-suite -> test_suite to make coq happy

---
 mathcomp/Make                        |   2 +-
 mathcomp/test-suite/hierarchy_test.v | 719 -----------------------------------
 mathcomp/test_suite/hierarchy_test.v | 719 +++++++++++++++++++++++++++++++++++
 3 files changed, 720 insertions(+), 720 deletions(-)
 delete mode 100644 mathcomp/test-suite/hierarchy_test.v
 create mode 100644 mathcomp/test_suite/hierarchy_test.v

(limited to 'mathcomp')

diff --git a/mathcomp/Make b/mathcomp/Make
index 27bf34f..4becdcb 100644
--- a/mathcomp/Make
+++ b/mathcomp/Make
@@ -87,7 +87,7 @@ ssreflect/ssrnat.v
 ssreflect/ssrnotations.v
 ssreflect/ssrmatching.v
 ssreflect/tuple.v
-test-suite/hierarchy_test.v
+test_suite/hierarchy_test.v
 
 -I .
 -R . mathcomp
diff --git a/mathcomp/test-suite/hierarchy_test.v b/mathcomp/test-suite/hierarchy_test.v
deleted file mode 100644
index a2bbf37..0000000
--- a/mathcomp/test-suite/hierarchy_test.v
+++ /dev/null
@@ -1,719 +0,0 @@
-(** Generated by etc/utils/hierarchy_test.py *)
-From mathcomp Require Import all.
-Local Notation "FinRing.UnitAlgebra.type" := (FinRing.UnitAlgebra.type _).
-Local Notation "GRing.Lalgebra.type" := (GRing.Lalgebra.type _).
-Local Notation "FinRing.Lalgebra.type" := (FinRing.Lalgebra.type _).
-Local Notation "FinRing.Algebra.type" := (FinRing.Algebra.type _).
-Local Notation "FieldExt.type" := (FieldExt.type _).
-Local Notation "GRing.UnitAlgebra.type" := (GRing.UnitAlgebra.type _).
-Local Notation "FinRing.Lmodule.type" := (FinRing.Lmodule.type _).
-Local Notation "GRing.Algebra.type" := (GRing.Algebra.type _).
-Local Notation "SplittingField.type" := (SplittingField.type _).
-Local Notation "Falgebra.type" := (Falgebra.type _).
-Local Notation "GRing.Lmodule.type" := (GRing.Lmodule.type _).
-Local Notation "Vector.type" := (Vector.type _).
-
-Check erefl : (_ : CountRing.ComRing.type) = (_ : FinGroup.type) :> Type.
-Check erefl : (_ : FieldExt.type) = (_ : SplittingField.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : Num.NumField.type) = (_ : Num.RealClosedField.type) :> Type.
-Check erefl : (_ : FinRing.Lalgebra.type) = (_ : FinRing.Ring.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : Num.ArchimedeanField.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : Countable.type) :> Type.
-Check erefl : (_ : Num.NumField.type) = (_ : Num.RealDomain.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : FinRing.Lmodule.type) :> Type.
-Check erefl : (_ : GRing.Lmodule.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : CountRing.Field.type) = (_ : Countable.type) :> Type.
-Check erefl : (_ : FinRing.Lalgebra.type) = (_ : Finite.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : FinRing.ComRing.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : FinRing.Lmodule.type) :> Type.
-Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.Lalgebra.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.Field.type) :> Type.
-Check erefl : (_ : GRing.Ring.type) = (_ : Num.NumDomain.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.UnitRing.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : Num.ClosedField.type) :> Type.
-Check erefl : (_ : FinRing.Algebra.type) = (_ : GRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : GRing.UnitAlgebra.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.Ring.type) :> Type.
-Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : FinGroup.type) = (_ : FinRing.Lalgebra.type) :> Type.
-Check erefl : (_ : GRing.ClosedField.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : GRing.ComRing.type) = (_ : Num.ArchimedeanField.type) :> Type.
-Check erefl : (_ : GRing.Field.type) = (_ : Num.ArchimedeanField.type) :> Type.
-Check erefl : (_ : GRing.Lalgebra.type) = (_ : Vector.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : Num.ClosedField.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : FinGroup.type) :> Type.
-Check erefl : (_ : GRing.UnitRing.type) = (_ : Num.RealField.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : Finite.type) :> Type.
-Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : Finite.type) :> Type.
-Check erefl : (_ : GRing.Ring.type) = (_ : Num.RealDomain.type) :> Type.
-Check erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.Lmodule.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : GRing.DecidableField.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : FinRing.Field.type) :> Type.
-Check erefl : (_ : FieldExt.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : CountRing.Field.type) = (_ : FinRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : Equality.type) :> Type.
-Check erefl : (_ : FinGroup.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : CountRing.UnitRing.type) :> Type.
-Check erefl : (_ : FinGroup.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.NumDomain.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : FinRing.UnitRing.type) :> Type.
-Check erefl : (_ : FinRing.ComRing.type) = (_ : Finite.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.DecidableField.type) :> Type.
-Check erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : Countable.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : CountRing.Field.type) = (_ : FinRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.UnitRing.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : Finite.type) :> Type.
-Check erefl : (_ : GRing.Lmodule.type) = (_ : GRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : Finite.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.ClosedField.type) :> Type.
-Check erefl : (_ : Finite.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : Equality.type) :> Type.
-Check erefl : (_ : FinGroup.type) = (_ : FinRing.Field.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : Num.RealField.type) :> Type.
-Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.Lalgebra.type) :> Type.
-Check erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : FieldExt.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.DecidableField.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : FieldExt.type) :> Type.
-Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.Lmodule.type) :> Type.
-Check erefl : (_ : GRing.DecidableField.type) = (_ : Num.NumDomain.type) :> Type.
-Check erefl : (_ : GRing.DecidableField.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : Countable.type) :> Type.
-Check erefl : (_ : FinRing.Lmodule.type) = (_ : FinRing.Ring.type) :> Type.
-Check erefl : (_ : FieldExt.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : GRing.UnitAlgebra.type) = (_ : Vector.type) :> Type.
-Check erefl : (_ : GRing.UnitRing.type) = (_ : Vector.type) :> Type.
-Check erefl : (_ : FinRing.Lalgebra.type) = (_ : FinRing.Lmodule.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Ring.type) :> Type.
-Check erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.RealClosedField.type) :> Type.
-Check erefl : (_ : CountRing.Field.type) = (_ : FinRing.ComRing.type) :> Type.
-Check erefl : (_ : GRing.IntegralDomain.type) = (_ : Vector.type) :> Type.
-Check erefl : (_ : FinRing.Algebra.type) = (_ : GRing.Lmodule.type) :> Type.
-Check erefl : (_ : GRing.Field.type) = (_ : GRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : Finite.type) :> Type.
-Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.DecidableField.type) :> Type.
-Check erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.Lalgebra.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : Equality.type) :> Type.
-Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : GRing.Field.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : FieldExt.type) = (_ : GRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : FinGroup.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : Num.RealClosedField.type) = (_ : Num.RealField.type) :> Type.
-Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.Ring.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.UnitRing.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : FinRing.Ring.type) :> Type.
-Check erefl : (_ : FinGroup.type) = (_ : FinRing.Ring.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.Ring.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : FinRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : GRing.DecidableField.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.ComRing.type) :> Type.
-Check erefl : (_ : GRing.Ring.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : Num.RealDomain.type) = (_ : Num.RealField.type) :> Type.
-Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.DecidableField.type) :> Type.
-Check erefl : (_ : FinRing.ComRing.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.ComRing.type) :> Type.
-Check erefl : (_ : GRing.DecidableField.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinGroup.type) :> Type.
-Check erefl : (_ : FinRing.Ring.type) = (_ : FinRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.Lmodule.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : FinRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.ComRing.type) :> Type.
-Check erefl : (_ : Falgebra.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : CountRing.ClosedField.type) :> Type.
-Check erefl : (_ : Finite.type) = (_ : GRing.ComRing.type) :> Type.
-Check erefl : (_ : GRing.ClosedField.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : Equality.type) :> Type.
-Check erefl : (_ : Falgebra.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : CountRing.DecidableField.type) = (_ : Equality.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : GRing.Lmodule.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : Finite.type) :> Type.
-Check erefl : (_ : FinRing.Field.type) = (_ : Finite.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.ClosedField.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Zmodule.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : Finite.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : CountRing.DecidableField.type) :> Type.
-Check erefl : (_ : Falgebra.type) = (_ : GRing.Algebra.type) :> Type.
-Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.ComRing.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.ComRing.type) :> Type.
-Check erefl : (_ : FinRing.Lmodule.type) = (_ : FinRing.Zmodule.type) :> Type.
-Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : FinRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : CountRing.DecidableField.type) = (_ : CountRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : FinRing.Lmodule.type) = (_ : Finite.type) :> Type.
-Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : CountRing.Field.type) = (_ : FinRing.Ring.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.ComRing.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : GRing.ComRing.type) :> Type.
-Check erefl : (_ : GRing.ComRing.type) = (_ : Num.NumField.type) :> Type.
-Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : FieldExt.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : CountRing.ComRing.type) :> Type.
-Check erefl : (_ : GRing.Field.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : FinRing.Field.type) = (_ : FinRing.Zmodule.type) :> Type.
-Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : FinRing.Zmodule.type) :> Type.
-Check erefl : (_ : GRing.Ring.type) = (_ : Num.RealField.type) :> Type.
-Check erefl : (_ : FieldExt.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : GRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : FinRing.UnitRing.type) :> Type.
-Check erefl : (_ : GRing.UnitRing.type) = (_ : SplittingField.type) :> Type.
-Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : FinGroup.type) = (_ : FinRing.Algebra.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : CountRing.UnitRing.type) :> Type.
-Check erefl : (_ : Falgebra.type) = (_ : SplittingField.type) :> Type.
-Check erefl : (_ : GRing.Lalgebra.type) = (_ : GRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : FieldExt.type) = (_ : GRing.Algebra.type) :> Type.
-Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.ComRing.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.ComRing.type) :> Type.
-Check erefl : (_ : GRing.DecidableField.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : CountRing.Field.type) = (_ : GRing.ComRing.type) :> Type.
-Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.Ring.type) :> Type.
-Check erefl : (_ : Num.NumDomain.type) = (_ : Num.RealField.type) :> Type.
-Check erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : CountRing.ClosedField.type) = (_ : Equality.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : GRing.ClosedField.type) :> Type.
-Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : Finite.type) = (_ : GRing.Lmodule.type) :> Type.
-Check erefl : (_ : GRing.ComUnitRing.type) = (_ : Vector.type) :> Type.
-Check erefl : (_ : GRing.ClosedField.type) = (_ : GRing.DecidableField.type) :> Type.
-Check erefl : (_ : FinRing.ComRing.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.Field.type) :> Type.
-Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : Equality.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : Num.RealField.type) :> Type.
-Check erefl : (_ : Num.ClosedField.type) = (_ : Num.NumField.type) :> Type.
-Check erefl : (_ : Num.NumDomain.type) = (_ : Num.RealDomain.type) :> Type.
-Check erefl : (_ : FinRing.Field.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.DecidableField.type) :> Type.
-Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.Lmodule.type) :> Type.
-Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : GRing.Lmodule.type) = (_ : SplittingField.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : FinRing.Field.type) :> Type.
-Check erefl : (_ : Falgebra.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.DecidableField.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.Zmodule.type) :> Type.
-Check erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.UnitRing.type) :> Type.
-Check erefl : (_ : FinRing.Field.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : GRing.Zmodule.type) = (_ : SplittingField.type) :> Type.
-Check erefl : (_ : FinRing.Algebra.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : FinRing.Zmodule.type) :> Type.
-Check erefl : (_ : GRing.UnitRing.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : FinRing.Algebra.type) :> Type.
-Check erefl : (_ : GRing.Zmodule.type) = (_ : Num.RealClosedField.type) :> Type.
-Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : GRing.Lalgebra.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : GRing.Ring.type) = (_ : Num.RealClosedField.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Field.type) :> Type.
-Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : GRing.Ring.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Lalgebra.type) :> Type.
-Check erefl : (_ : GRing.Field.type) = (_ : Num.ClosedField.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.Zmodule.type) :> Type.
-Check erefl : (_ : FinRing.Field.type) = (_ : GRing.ComRing.type) :> Type.
-Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : FinRing.Lalgebra.type) :> Type.
-Check erefl : (_ : Num.ArchimedeanField.type) = (_ : Num.NumField.type) :> Type.
-Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : Falgebra.type) :> Type.
-Check erefl : (_ : GRing.Zmodule.type) = (_ : Num.RealDomain.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : Num.NumDomain.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.Zmodule.type) :> Type.
-Check erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.Algebra.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : GRing.Algebra.type) :> Type.
-Check erefl : (_ : FinRing.Lmodule.type) = (_ : FinRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : Num.ArchimedeanField.type) = (_ : Num.RealDomain.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.DecidableField.type) :> Type.
-Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Algebra.type) :> Type.
-Check erefl : (_ : GRing.Lmodule.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : FinGroup.type) = (_ : GRing.Lalgebra.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : FinRing.Lmodule.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : FinRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : CountRing.Ring.type) :> Type.
-Check erefl : (_ : GRing.UnitAlgebra.type) = (_ : SplittingField.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : GRing.DecidableField.type) :> Type.
-Check erefl : (_ : FieldExt.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : FinRing.Field.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : GRing.Lalgebra.type) :> Type.
-Check erefl : (_ : GRing.Algebra.type) = (_ : SplittingField.type) :> Type.
-Check erefl : (_ : FinGroup.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : FinRing.Algebra.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Ring.type) :> Type.
-Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.Lmodule.type) :> Type.
-Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.ComRing.type) :> Type.
-Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Lmodule.type) :> Type.
-Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : GRing.ComRing.type) = (_ : Num.NumDomain.type) :> Type.
-Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.Field.type) :> Type.
-Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : FinRing.Zmodule.type) :> Type.
-Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.Algebra.type) :> Type.
-Check erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : CountRing.Field.type) = (_ : FinRing.UnitRing.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : FinRing.ComRing.type) :> Type.
-Check erefl : (_ : GRing.Field.type) = (_ : Vector.type) :> Type.
-Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : GRing.Zmodule.type) = (_ : Num.RealField.type) :> Type.
-Check erefl : (_ : GRing.Ring.type) = (_ : Num.NumField.type) :> Type.
-Check erefl : (_ : GRing.ClosedField.type) = (_ : GRing.ComRing.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : Finite.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Field.type) :> Type.
-Check erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.Zmodule.type) :> Type.
-Check erefl : (_ : FinRing.Field.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.ClosedField.type) :> Type.
-Check erefl : (_ : Num.NumField.type) = (_ : Num.RealField.type) :> Type.
-Check erefl : (_ : GRing.Ring.type) = (_ : Num.ArchimedeanField.type) :> Type.
-Check erefl : (_ : GRing.UnitRing.type) = (_ : Num.RealDomain.type) :> Type.
-Check erefl : (_ : FinGroup.type) = (_ : GRing.ComRing.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : FinGroup.type) :> Type.
-Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : GRing.Ring.type) = (_ : Num.ClosedField.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinGroup.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : FinRing.ComRing.type) :> Type.
-Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.ComRing.type) :> Type.
-Check erefl : (_ : GRing.Field.type) = (_ : Num.NumField.type) :> Type.
-Check erefl : (_ : FinRing.Zmodule.type) = (_ : Finite.type) :> Type.
-Check erefl : (_ : GRing.Zmodule.type) = (_ : Num.ClosedField.type) :> Type.
-Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.ComRing.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.DecidableField.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : Equality.type) :> Type.
-Check erefl : (_ : Falgebra.type) = (_ : FieldExt.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.UnitRing.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.ClosedField.type) :> Type.
-Check erefl : (_ : GRing.Lmodule.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : GRing.Zmodule.type) = (_ : Num.NumField.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : FinRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : CountRing.Field.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : CountRing.Field.type) = (_ : CountRing.Ring.type) :> Type.
-Check erefl : (_ : FieldExt.type) = (_ : GRing.Lalgebra.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : GRing.Lmodule.type) :> Type.
-Check erefl : (_ : FinGroup.type) = (_ : FinRing.UnitRing.type) :> Type.
-Check erefl : (_ : GRing.ComUnitRing.type) = (_ : SplittingField.type) :> Type.
-Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.DecidableField.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinGroup.type) :> Type.
-Check erefl : (_ : CountRing.Field.type) = (_ : FinGroup.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.Zmodule.type) :> Type.
-Check erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.UnitRing.type) :> Type.
-Check erefl : (_ : FinRing.Lmodule.type) = (_ : FinRing.UnitRing.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : GRing.Lmodule.type) :> Type.
-Check erefl : (_ : GRing.Field.type) = (_ : Num.RealField.type) :> Type.
-Check erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : GRing.UnitRing.type) = (_ : Num.RealClosedField.type) :> Type.
-Check erefl : (_ : Finite.type) = (_ : GRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : GRing.UnitRing.type) = (_ : Num.ArchimedeanField.type) :> Type.
-Check erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.Ring.type) :> Type.
-Check erefl : (_ : FinRing.Algebra.type) = (_ : Finite.type) :> Type.
-Check erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.NumDomain.type) :> Type.
-Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.ArchimedeanField.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : CountRing.Ring.type) :> Type.
-Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : Finite.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Lmodule.type) :> Type.
-Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : CountRing.DecidableField.type) = (_ : CountRing.Ring.type) :> Type.
-Check erefl : (_ : GRing.Lalgebra.type) = (_ : SplittingField.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.ComRing.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : GRing.DecidableField.type) = (_ : Num.NumField.type) :> Type.
-Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : GRing.UnitRing.type) = (_ : Num.ClosedField.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : Finite.type) :> Type.
-Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : Finite.type) :> Type.
-Check erefl : (_ : FieldExt.type) = (_ : GRing.ComRing.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : Num.RealDomain.type) :> Type.
-Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.Zmodule.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : FinRing.Zmodule.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : GRing.Field.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : CountRing.Field.type) = (_ : GRing.ClosedField.type) :> Type.
-Check erefl : (_ : GRing.Field.type) = (_ : GRing.Lmodule.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : FinRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : Falgebra.type) = (_ : GRing.Lmodule.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : Finite.type) = (_ : GRing.Lalgebra.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.RealField.type) :> Type.
-Check erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.NumField.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : Num.NumField.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.ComRing.type) :> Type.
-Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.ClosedField.type) :> Type.
-Check erefl : (_ : SplittingField.type) = (_ : Vector.type) :> Type.
-Check erefl : (_ : Finite.type) = (_ : GRing.Algebra.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : GRing.Field.type) = (_ : SplittingField.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : CountRing.Field.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.UnitRing.type) :> Type.
-Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : FinRing.Ring.type) :> Type.
-Check erefl : (_ : FinRing.UnitRing.type) = (_ : FinRing.Zmodule.type) :> Type.
-Check erefl : (_ : FinRing.Ring.type) = (_ : FinRing.Zmodule.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : Num.NumField.type) :> Type.
-Check erefl : (_ : GRing.ClosedField.type) = (_ : Num.NumField.type) :> Type.
-Check erefl : (_ : GRing.ComRing.type) = (_ : SplittingField.type) :> Type.
-Check erefl : (_ : GRing.ClosedField.type) = (_ : Num.NumDomain.type) :> Type.
-Check erefl : (_ : GRing.ComRing.type) = (_ : Num.RealDomain.type) :> Type.
-Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.Lmodule.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.RealField.type) :> Type.
-Check erefl : (_ : Num.RealClosedField.type) = (_ : Num.RealDomain.type) :> Type.
-Check erefl : (_ : Finite.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : FinRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.ClosedField.type) :> Type.
-Check erefl : (_ : FinGroup.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.RealClosedField.type) :> Type.
-Check erefl : (_ : Finite.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : FieldExt.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : GRing.Field.type) = (_ : GRing.Lalgebra.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : FinRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : GRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : CountRing.Field.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.ClosedField.type) :> Type.
-Check erefl : (_ : CountRing.Field.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : GRing.ClosedField.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : Vector.type) :> Type.
-Check erefl : (_ : GRing.Lalgebra.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.ComRing.type) :> Type.
-Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : CountRing.Zmodule.type) :> Type.
-Check erefl : (_ : FinRing.Ring.type) = (_ : FinRing.UnitRing.type) :> Type.
-Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : Countable.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : CountRing.Zmodule.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : SplittingField.type) :> Type.
-Check erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.Lalgebra.type) :> Type.
-Check erefl : (_ : FinRing.ComRing.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : FinRing.Lalgebra.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : GRing.DecidableField.type) = (_ : Num.ClosedField.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : GRing.ComRing.type) = (_ : Num.RealField.type) :> Type.
-Check erefl : (_ : GRing.ClosedField.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.ComRing.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : FinRing.UnitRing.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.ComRing.type) :> Type.
-Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : SplittingField.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : FinRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : CountRing.Field.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : GRing.Zmodule.type) = (_ : Vector.type) :> Type.
-Check erefl : (_ : CountRing.Field.type) = (_ : CountRing.Zmodule.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : FinRing.Field.type) :> Type.
-Check erefl : (_ : Falgebra.type) = (_ : GRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : FinRing.Algebra.type) = (_ : GRing.Algebra.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.Lalgebra.type) :> Type.
-Check erefl : (_ : GRing.Zmodule.type) = (_ : Num.NumDomain.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.Algebra.type) :> Type.
-Check erefl : (_ : FinGroup.type) = (_ : FinRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : Vector.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : FinRing.Zmodule.type) :> Type.
-Check erefl : (_ : Falgebra.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : Num.NumDomain.type) = (_ : Num.RealClosedField.type) :> Type.
-Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : FinRing.UnitRing.type) :> Type.
-Check erefl : (_ : CountRing.DecidableField.type) = (_ : CountRing.UnitRing.type) :> Type.
-Check erefl : (_ : FinGroup.type) = (_ : FinRing.Lmodule.type) :> Type.
-Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.UnitRing.type) :> Type.
-Check erefl : (_ : FieldExt.type) = (_ : GRing.Lmodule.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : FinGroup.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : CountRing.Field.type) = (_ : Finite.type) :> Type.
-Check erefl : (_ : FinGroup.type) = (_ : FinRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : GRing.Field.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : CountRing.Field.type) = (_ : CountRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : Num.ArchimedeanField.type) = (_ : Num.RealField.type) :> Type.
-Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.Algebra.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : FinRing.Lalgebra.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.Field.type) :> Type.
-Check erefl : (_ : GRing.UnitAlgebra.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : CountRing.Field.type) = (_ : FinRing.Field.type) :> Type.
-Check erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.Lmodule.type) :> Type.
-Check erefl : (_ : CountRing.Field.type) = (_ : CountRing.UnitRing.type) :> Type.
-Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : GRing.ComRing.type) = (_ : Vector.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : CountRing.Zmodule.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : FinGroup.type) = (_ : GRing.Algebra.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Zmodule.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.Ring.type) :> Type.
-Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.Lalgebra.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Lalgebra.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : GRing.Lalgebra.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : Finite.type) :> Type.
-Check erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.Lalgebra.type) :> Type.
-Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : GRing.ClosedField.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : GRing.Lalgebra.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : GRing.ComRing.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : CountRing.Field.type) = (_ : FinRing.Zmodule.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : Num.NumDomain.type) :> Type.
-Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : FinRing.UnitRing.type) :> Type.
-Check erefl : (_ : FinRing.UnitRing.type) = (_ : Finite.type) :> Type.
-Check erefl : (_ : FinGroup.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : FinRing.Lalgebra.type) = (_ : FinRing.UnitRing.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Lmodule.type) :> Type.
-Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : FinRing.Field.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Lmodule.type) :> Type.
-Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinGroup.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.UnitRing.type) :> Type.
-Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.ComRing.type) :> Type.
-Check erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Lalgebra.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : FinRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : GRing.DecidableField.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Field.type) :> Type.
-Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : FinGroup.type) = (_ : FinRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : GRing.Ring.type) = (_ : Vector.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : FinRing.Algebra.type) :> Type.
-Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : Finite.type) :> Type.
-Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.DecidableField.type) :> Type.
-Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : FinRing.Field.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Ring.type) :> Type.
-Check erefl : (_ : Num.ArchimedeanField.type) = (_ : Num.NumDomain.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : FinRing.Zmodule.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : GRing.ComRing.type) :> Type.
-Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : CountRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.Field.type) :> Type.
-Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.Zmodule.type) :> Type.
-Check erefl : (_ : CountRing.ClosedField.type) = (_ : Countable.type) :> Type.
-Check erefl : (_ : CountRing.DecidableField.type) = (_ : CountRing.Field.type) :> Type.
-Check erefl : (_ : CountRing.Field.type) = (_ : Equality.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : FinRing.ComRing.type) :> Type.
-Check erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : CountRing.Field.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : CountRing.Field.type) :> Type.
-Check erefl : (_ : GRing.Field.type) = (_ : Num.RealClosedField.type) :> Type.
-Check erefl : (_ : FinRing.Field.type) = (_ : FinRing.Ring.type) :> Type.
-Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Lalgebra.type) :> Type.
-Check erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.Ring.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : CountRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : FinRing.Field.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Algebra.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : CountRing.Zmodule.type) :> Type.
-Check erefl : (_ : CountRing.DecidableField.type) = (_ : Countable.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : Countable.type) :> Type.
-Check erefl : (_ : CountRing.DecidableField.type) = (_ : CountRing.Zmodule.type) :> Type.
-Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : FinRing.Ring.type) :> Type.
-Check erefl : (_ : FinGroup.type) = (_ : FinRing.ComRing.type) :> Type.
-Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.ComRing.type) :> Type.
-Check erefl : (_ : Falgebra.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : FinRing.Lalgebra.type) = (_ : FinRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.Lalgebra.type) :> Type.
-Check erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.Zmodule.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.Lmodule.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.ClosedField.type) :> Type.
-Check erefl : (_ : GRing.Lalgebra.type) = (_ : GRing.Lmodule.type) :> Type.
-Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.Lalgebra.type) :> Type.
-Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Zmodule.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Algebra.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : Countable.type) :> Type.
-Check erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.RealDomain.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.DecidableField.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : GRing.UnitRing.type) = (_ : Num.NumField.type) :> Type.
-Check erefl : (_ : GRing.DecidableField.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : GRing.ClosedField.type) = (_ : Num.ClosedField.type) :> Type.
-Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.ComRing.type) :> Type.
-Check erefl : (_ : FinGroup.type) = (_ : Finite.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : FinRing.UnitRing.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Algebra.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Lalgebra.type) :> Type.
-Check erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.Algebra.type) :> Type.
-Check erefl : (_ : FinRing.Ring.type) = (_ : Finite.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : Num.RealDomain.type) :> Type.
-Check erefl : (_ : Falgebra.type) = (_ : GRing.ComRing.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : GRing.Algebra.type) :> Type.
-Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : GRing.ComRing.type) = (_ : Num.RealClosedField.type) :> Type.
-Check erefl : (_ : GRing.IntegralDomain.type) = (_ : SplittingField.type) :> Type.
-Check erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : Falgebra.type) = (_ : GRing.Lalgebra.type) :> Type.
-Check erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.NumField.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : Falgebra.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.ClosedField.type) :> Type.
-Check erefl : (_ : GRing.ComRing.type) = (_ : Num.ClosedField.type) :> Type.
-Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.Field.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : Finite.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Lmodule.type) :> Type.
-Check erefl : (_ : FinRing.Lalgebra.type) = (_ : FinRing.Zmodule.type) :> Type.
-Check erefl : (_ : GRing.Lalgebra.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : GRing.UnitRing.type) = (_ : Num.NumDomain.type) :> Type.
-Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.Field.type) :> Type.
-Check erefl : (_ : Num.ClosedField.type) = (_ : Num.NumDomain.type) :> Type.
-Check erefl : (_ : FinRing.Field.type) = (_ : FinRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.ArchimedeanField.type) :> Type.
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : Equality.type) :> Type.
-Check erefl : (_ : Falgebra.type) = (_ : Vector.type) :> Type.
-Check erefl : (_ : GRing.Lmodule.type) = (_ : Vector.type) :> Type.
-Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : CountRing.UnitRing.type) :> Type.
-Check erefl : (_ : FinRing.Field.type) = (_ : FinRing.UnitRing.type) :> Type.
-Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : FinRing.ComRing.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : GRing.Ring.type) = (_ : SplittingField.type) :> Type.
-Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : FinGroup.type) = (_ : GRing.Lmodule.type) :> Type.
-Check erefl : (_ : CountRing.Field.type) = (_ : GRing.DecidableField.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : Countable.type) :> Type.
-Check erefl : (_ : FinGroup.type) = (_ : FinRing.Zmodule.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.UnitRing.type) :> Type.
-Check erefl : (_ : GRing.ClosedField.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : Num.NumDomain.type) = (_ : Num.NumField.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : FinRing.Ring.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : Num.ArchimedeanField.type) :> Type.
-Check erefl : (_ : FinGroup.type) = (_ : GRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.Field.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.DecidableField.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.Lalgebra.type) :> Type.
-Check erefl : (_ : FinRing.ComRing.type) = (_ : GRing.ComRing.type) :> Type.
-Check erefl : (_ : Falgebra.type) = (_ : GRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : GRing.ClosedField.type) :> Type.
-Check erefl : (_ : FieldExt.type) = (_ : Vector.type) :> Type.
-Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : Finite.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.Zmodule.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.DecidableField.type) :> Type.
-Check erefl : (_ : CountRing.Ring.type) = (_ : FinGroup.type) :> Type.
-Check erefl : (_ : Equality.type) = (_ : Num.RealClosedField.type) :> Type.
-Check erefl : (_ : GRing.Algebra.type) = (_ : Vector.type) :> Type.
-Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.ComRing.type) :> Type.
-Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.ComUnitRing.type) :> Type.
-Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : FinRing.Ring.type) :> Type.
-Check erefl : (_ : GRing.Ring.type) = (_ : GRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.Ring.type) :> Type.
-Check erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.ClosedField.type) :> Type.
-Check erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.Lmodule.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : GRing.Algebra.type) :> Type.
-Check erefl : (_ : FinRing.Algebra.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.RealDomain.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : FinRing.Algebra.type) :> Type.
-Check erefl : (_ : FinRing.Algebra.type) = (_ : GRing.Lalgebra.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : Num.RealClosedField.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : Equality.type) :> Type.
-Check erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.Lmodule.type) :> Type.
-Check erefl : (_ : FinRing.ComRing.type) = (_ : GRing.UnitRing.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : GRing.ClosedField.type) :> Type.
-Check erefl : (_ : Countable.type) = (_ : GRing.Ring.type) :> Type.
-Check erefl : (_ : Choice.type) = (_ : GRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.UnitAlgebra.type) :> Type.
-Check erefl : (_ : GRing.Zmodule.type) = (_ : Num.ArchimedeanField.type) :> Type.
-
-(* fix in ssrnum *)
-Check erefl : (_ : GRing.Field.type) = (_ : Num.NumDomain.type) :> Type.
-Check erefl : (_ : GRing.Field.type) = (_ : Num.RealDomain.type) :> Type.
-
-(* fix in countalg *)
-Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.IntegralDomain.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Lmodule.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Algebra.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Lalgebra.type) :> Type.
-
-(* fix in finalg *)
-Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Algebra.type) :> Type.
-Check erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.UnitRing.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Algebra.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Lalgebra.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Lmodule.type) :> Type.
-Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.ComRing.type) :> Type.
diff --git a/mathcomp/test_suite/hierarchy_test.v b/mathcomp/test_suite/hierarchy_test.v
new file mode 100644
index 0000000..a2bbf37
--- /dev/null
+++ b/mathcomp/test_suite/hierarchy_test.v
@@ -0,0 +1,719 @@
+(** Generated by etc/utils/hierarchy_test.py *)
+From mathcomp Require Import all.
+Local Notation "FinRing.UnitAlgebra.type" := (FinRing.UnitAlgebra.type _).
+Local Notation "GRing.Lalgebra.type" := (GRing.Lalgebra.type _).
+Local Notation "FinRing.Lalgebra.type" := (FinRing.Lalgebra.type _).
+Local Notation "FinRing.Algebra.type" := (FinRing.Algebra.type _).
+Local Notation "FieldExt.type" := (FieldExt.type _).
+Local Notation "GRing.UnitAlgebra.type" := (GRing.UnitAlgebra.type _).
+Local Notation "FinRing.Lmodule.type" := (FinRing.Lmodule.type _).
+Local Notation "GRing.Algebra.type" := (GRing.Algebra.type _).
+Local Notation "SplittingField.type" := (SplittingField.type _).
+Local Notation "Falgebra.type" := (Falgebra.type _).
+Local Notation "GRing.Lmodule.type" := (GRing.Lmodule.type _).
+Local Notation "Vector.type" := (Vector.type _).
+
+Check erefl : (_ : CountRing.ComRing.type) = (_ : FinGroup.type) :> Type.
+Check erefl : (_ : FieldExt.type) = (_ : SplittingField.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : Num.NumField.type) = (_ : Num.RealClosedField.type) :> Type.
+Check erefl : (_ : FinRing.Lalgebra.type) = (_ : FinRing.Ring.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : Num.ArchimedeanField.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : Countable.type) :> Type.
+Check erefl : (_ : Num.NumField.type) = (_ : Num.RealDomain.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : FinRing.Lmodule.type) :> Type.
+Check erefl : (_ : GRing.Lmodule.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : CountRing.Field.type) = (_ : Countable.type) :> Type.
+Check erefl : (_ : FinRing.Lalgebra.type) = (_ : Finite.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : FinRing.ComRing.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : FinRing.Lmodule.type) :> Type.
+Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.Lalgebra.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.Field.type) :> Type.
+Check erefl : (_ : GRing.Ring.type) = (_ : Num.NumDomain.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.UnitRing.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : Num.ClosedField.type) :> Type.
+Check erefl : (_ : FinRing.Algebra.type) = (_ : GRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : GRing.UnitAlgebra.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.Ring.type) :> Type.
+Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : FinGroup.type) = (_ : FinRing.Lalgebra.type) :> Type.
+Check erefl : (_ : GRing.ClosedField.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : GRing.ComRing.type) = (_ : Num.ArchimedeanField.type) :> Type.
+Check erefl : (_ : GRing.Field.type) = (_ : Num.ArchimedeanField.type) :> Type.
+Check erefl : (_ : GRing.Lalgebra.type) = (_ : Vector.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : Num.ClosedField.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : FinGroup.type) :> Type.
+Check erefl : (_ : GRing.UnitRing.type) = (_ : Num.RealField.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : Finite.type) :> Type.
+Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : Finite.type) :> Type.
+Check erefl : (_ : GRing.Ring.type) = (_ : Num.RealDomain.type) :> Type.
+Check erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.Lmodule.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : GRing.DecidableField.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : FinRing.Field.type) :> Type.
+Check erefl : (_ : FieldExt.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : CountRing.Field.type) = (_ : FinRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : Equality.type) :> Type.
+Check erefl : (_ : FinGroup.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : CountRing.UnitRing.type) :> Type.
+Check erefl : (_ : FinGroup.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.NumDomain.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : FinRing.UnitRing.type) :> Type.
+Check erefl : (_ : FinRing.ComRing.type) = (_ : Finite.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.DecidableField.type) :> Type.
+Check erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : Countable.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : CountRing.Field.type) = (_ : FinRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.UnitRing.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : Finite.type) :> Type.
+Check erefl : (_ : GRing.Lmodule.type) = (_ : GRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : Finite.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.ClosedField.type) :> Type.
+Check erefl : (_ : Finite.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : Equality.type) :> Type.
+Check erefl : (_ : FinGroup.type) = (_ : FinRing.Field.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : Num.RealField.type) :> Type.
+Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.Lalgebra.type) :> Type.
+Check erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : FieldExt.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.DecidableField.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : FieldExt.type) :> Type.
+Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.Lmodule.type) :> Type.
+Check erefl : (_ : GRing.DecidableField.type) = (_ : Num.NumDomain.type) :> Type.
+Check erefl : (_ : GRing.DecidableField.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : Countable.type) :> Type.
+Check erefl : (_ : FinRing.Lmodule.type) = (_ : FinRing.Ring.type) :> Type.
+Check erefl : (_ : FieldExt.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : GRing.UnitAlgebra.type) = (_ : Vector.type) :> Type.
+Check erefl : (_ : GRing.UnitRing.type) = (_ : Vector.type) :> Type.
+Check erefl : (_ : FinRing.Lalgebra.type) = (_ : FinRing.Lmodule.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Ring.type) :> Type.
+Check erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.RealClosedField.type) :> Type.
+Check erefl : (_ : CountRing.Field.type) = (_ : FinRing.ComRing.type) :> Type.
+Check erefl : (_ : GRing.IntegralDomain.type) = (_ : Vector.type) :> Type.
+Check erefl : (_ : FinRing.Algebra.type) = (_ : GRing.Lmodule.type) :> Type.
+Check erefl : (_ : GRing.Field.type) = (_ : GRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : Finite.type) :> Type.
+Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.DecidableField.type) :> Type.
+Check erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.Lalgebra.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : Equality.type) :> Type.
+Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : GRing.Field.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : FieldExt.type) = (_ : GRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : FinGroup.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : Num.RealClosedField.type) = (_ : Num.RealField.type) :> Type.
+Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.Ring.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.UnitRing.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : FinRing.Ring.type) :> Type.
+Check erefl : (_ : FinGroup.type) = (_ : FinRing.Ring.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.Ring.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : FinRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : GRing.DecidableField.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.ComRing.type) :> Type.
+Check erefl : (_ : GRing.Ring.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : Num.RealDomain.type) = (_ : Num.RealField.type) :> Type.
+Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.DecidableField.type) :> Type.
+Check erefl : (_ : FinRing.ComRing.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.ComRing.type) :> Type.
+Check erefl : (_ : GRing.DecidableField.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinGroup.type) :> Type.
+Check erefl : (_ : FinRing.Ring.type) = (_ : FinRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.Lmodule.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : FinRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.ComRing.type) :> Type.
+Check erefl : (_ : Falgebra.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : CountRing.ClosedField.type) :> Type.
+Check erefl : (_ : Finite.type) = (_ : GRing.ComRing.type) :> Type.
+Check erefl : (_ : GRing.ClosedField.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : Equality.type) :> Type.
+Check erefl : (_ : Falgebra.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : CountRing.DecidableField.type) = (_ : Equality.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : GRing.Lmodule.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : Finite.type) :> Type.
+Check erefl : (_ : FinRing.Field.type) = (_ : Finite.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.ClosedField.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Zmodule.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : Finite.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : CountRing.DecidableField.type) :> Type.
+Check erefl : (_ : Falgebra.type) = (_ : GRing.Algebra.type) :> Type.
+Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.ComRing.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.ComRing.type) :> Type.
+Check erefl : (_ : FinRing.Lmodule.type) = (_ : FinRing.Zmodule.type) :> Type.
+Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : FinRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : CountRing.DecidableField.type) = (_ : CountRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : FinRing.Lmodule.type) = (_ : Finite.type) :> Type.
+Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : CountRing.Field.type) = (_ : FinRing.Ring.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.ComRing.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : GRing.ComRing.type) :> Type.
+Check erefl : (_ : GRing.ComRing.type) = (_ : Num.NumField.type) :> Type.
+Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : FieldExt.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : CountRing.ComRing.type) :> Type.
+Check erefl : (_ : GRing.Field.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : FinRing.Field.type) = (_ : FinRing.Zmodule.type) :> Type.
+Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : FinRing.Zmodule.type) :> Type.
+Check erefl : (_ : GRing.Ring.type) = (_ : Num.RealField.type) :> Type.
+Check erefl : (_ : FieldExt.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : GRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : FinRing.UnitRing.type) :> Type.
+Check erefl : (_ : GRing.UnitRing.type) = (_ : SplittingField.type) :> Type.
+Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : FinGroup.type) = (_ : FinRing.Algebra.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : CountRing.UnitRing.type) :> Type.
+Check erefl : (_ : Falgebra.type) = (_ : SplittingField.type) :> Type.
+Check erefl : (_ : GRing.Lalgebra.type) = (_ : GRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : FieldExt.type) = (_ : GRing.Algebra.type) :> Type.
+Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.ComRing.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.ComRing.type) :> Type.
+Check erefl : (_ : GRing.DecidableField.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : CountRing.Field.type) = (_ : GRing.ComRing.type) :> Type.
+Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.Ring.type) :> Type.
+Check erefl : (_ : Num.NumDomain.type) = (_ : Num.RealField.type) :> Type.
+Check erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : CountRing.ClosedField.type) = (_ : Equality.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : GRing.ClosedField.type) :> Type.
+Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : Finite.type) = (_ : GRing.Lmodule.type) :> Type.
+Check erefl : (_ : GRing.ComUnitRing.type) = (_ : Vector.type) :> Type.
+Check erefl : (_ : GRing.ClosedField.type) = (_ : GRing.DecidableField.type) :> Type.
+Check erefl : (_ : FinRing.ComRing.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.Field.type) :> Type.
+Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : Equality.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : Num.RealField.type) :> Type.
+Check erefl : (_ : Num.ClosedField.type) = (_ : Num.NumField.type) :> Type.
+Check erefl : (_ : Num.NumDomain.type) = (_ : Num.RealDomain.type) :> Type.
+Check erefl : (_ : FinRing.Field.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.DecidableField.type) :> Type.
+Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.Lmodule.type) :> Type.
+Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : GRing.Lmodule.type) = (_ : SplittingField.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : FinRing.Field.type) :> Type.
+Check erefl : (_ : Falgebra.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.DecidableField.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.Zmodule.type) :> Type.
+Check erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.UnitRing.type) :> Type.
+Check erefl : (_ : FinRing.Field.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : GRing.Zmodule.type) = (_ : SplittingField.type) :> Type.
+Check erefl : (_ : FinRing.Algebra.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : FinRing.Zmodule.type) :> Type.
+Check erefl : (_ : GRing.UnitRing.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : FinRing.Algebra.type) :> Type.
+Check erefl : (_ : GRing.Zmodule.type) = (_ : Num.RealClosedField.type) :> Type.
+Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : GRing.Lalgebra.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : GRing.Ring.type) = (_ : Num.RealClosedField.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Field.type) :> Type.
+Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : GRing.Ring.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Lalgebra.type) :> Type.
+Check erefl : (_ : GRing.Field.type) = (_ : Num.ClosedField.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.Zmodule.type) :> Type.
+Check erefl : (_ : FinRing.Field.type) = (_ : GRing.ComRing.type) :> Type.
+Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : FinRing.Lalgebra.type) :> Type.
+Check erefl : (_ : Num.ArchimedeanField.type) = (_ : Num.NumField.type) :> Type.
+Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : Falgebra.type) :> Type.
+Check erefl : (_ : GRing.Zmodule.type) = (_ : Num.RealDomain.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : Num.NumDomain.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.Zmodule.type) :> Type.
+Check erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.Algebra.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : GRing.Algebra.type) :> Type.
+Check erefl : (_ : FinRing.Lmodule.type) = (_ : FinRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : Num.ArchimedeanField.type) = (_ : Num.RealDomain.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.DecidableField.type) :> Type.
+Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Algebra.type) :> Type.
+Check erefl : (_ : GRing.Lmodule.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : FinGroup.type) = (_ : GRing.Lalgebra.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : FinRing.Lmodule.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : FinRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : CountRing.Ring.type) :> Type.
+Check erefl : (_ : GRing.UnitAlgebra.type) = (_ : SplittingField.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : GRing.DecidableField.type) :> Type.
+Check erefl : (_ : FieldExt.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : FinRing.Field.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : GRing.Lalgebra.type) :> Type.
+Check erefl : (_ : GRing.Algebra.type) = (_ : SplittingField.type) :> Type.
+Check erefl : (_ : FinGroup.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : FinRing.Algebra.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Ring.type) :> Type.
+Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.Lmodule.type) :> Type.
+Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.ComRing.type) :> Type.
+Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Lmodule.type) :> Type.
+Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : GRing.ComRing.type) = (_ : Num.NumDomain.type) :> Type.
+Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.Field.type) :> Type.
+Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : FinRing.Zmodule.type) :> Type.
+Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.Algebra.type) :> Type.
+Check erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : CountRing.Field.type) = (_ : FinRing.UnitRing.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : FinRing.ComRing.type) :> Type.
+Check erefl : (_ : GRing.Field.type) = (_ : Vector.type) :> Type.
+Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : GRing.Zmodule.type) = (_ : Num.RealField.type) :> Type.
+Check erefl : (_ : GRing.Ring.type) = (_ : Num.NumField.type) :> Type.
+Check erefl : (_ : GRing.ClosedField.type) = (_ : GRing.ComRing.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : Finite.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Field.type) :> Type.
+Check erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.Zmodule.type) :> Type.
+Check erefl : (_ : FinRing.Field.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.ClosedField.type) :> Type.
+Check erefl : (_ : Num.NumField.type) = (_ : Num.RealField.type) :> Type.
+Check erefl : (_ : GRing.Ring.type) = (_ : Num.ArchimedeanField.type) :> Type.
+Check erefl : (_ : GRing.UnitRing.type) = (_ : Num.RealDomain.type) :> Type.
+Check erefl : (_ : FinGroup.type) = (_ : GRing.ComRing.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : FinGroup.type) :> Type.
+Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : GRing.Ring.type) = (_ : Num.ClosedField.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinGroup.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : FinRing.ComRing.type) :> Type.
+Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.ComRing.type) :> Type.
+Check erefl : (_ : GRing.Field.type) = (_ : Num.NumField.type) :> Type.
+Check erefl : (_ : FinRing.Zmodule.type) = (_ : Finite.type) :> Type.
+Check erefl : (_ : GRing.Zmodule.type) = (_ : Num.ClosedField.type) :> Type.
+Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.ComRing.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.DecidableField.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : Equality.type) :> Type.
+Check erefl : (_ : Falgebra.type) = (_ : FieldExt.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.UnitRing.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.ClosedField.type) :> Type.
+Check erefl : (_ : GRing.Lmodule.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : GRing.Zmodule.type) = (_ : Num.NumField.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : FinRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : CountRing.Field.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : CountRing.Field.type) = (_ : CountRing.Ring.type) :> Type.
+Check erefl : (_ : FieldExt.type) = (_ : GRing.Lalgebra.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : GRing.Lmodule.type) :> Type.
+Check erefl : (_ : FinGroup.type) = (_ : FinRing.UnitRing.type) :> Type.
+Check erefl : (_ : GRing.ComUnitRing.type) = (_ : SplittingField.type) :> Type.
+Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.DecidableField.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinGroup.type) :> Type.
+Check erefl : (_ : CountRing.Field.type) = (_ : FinGroup.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.Zmodule.type) :> Type.
+Check erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.UnitRing.type) :> Type.
+Check erefl : (_ : FinRing.Lmodule.type) = (_ : FinRing.UnitRing.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : GRing.Lmodule.type) :> Type.
+Check erefl : (_ : GRing.Field.type) = (_ : Num.RealField.type) :> Type.
+Check erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : GRing.UnitRing.type) = (_ : Num.RealClosedField.type) :> Type.
+Check erefl : (_ : Finite.type) = (_ : GRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : GRing.UnitRing.type) = (_ : Num.ArchimedeanField.type) :> Type.
+Check erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.Ring.type) :> Type.
+Check erefl : (_ : FinRing.Algebra.type) = (_ : Finite.type) :> Type.
+Check erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.NumDomain.type) :> Type.
+Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.ArchimedeanField.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : CountRing.Ring.type) :> Type.
+Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : Finite.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Lmodule.type) :> Type.
+Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : CountRing.DecidableField.type) = (_ : CountRing.Ring.type) :> Type.
+Check erefl : (_ : GRing.Lalgebra.type) = (_ : SplittingField.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.ComRing.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : GRing.DecidableField.type) = (_ : Num.NumField.type) :> Type.
+Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : GRing.UnitRing.type) = (_ : Num.ClosedField.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : Finite.type) :> Type.
+Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : Finite.type) :> Type.
+Check erefl : (_ : FieldExt.type) = (_ : GRing.ComRing.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : Num.RealDomain.type) :> Type.
+Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.Zmodule.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : FinRing.Zmodule.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : GRing.Field.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : CountRing.Field.type) = (_ : GRing.ClosedField.type) :> Type.
+Check erefl : (_ : GRing.Field.type) = (_ : GRing.Lmodule.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : FinRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : Falgebra.type) = (_ : GRing.Lmodule.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : Finite.type) = (_ : GRing.Lalgebra.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.RealField.type) :> Type.
+Check erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.NumField.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : Num.NumField.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.ComRing.type) :> Type.
+Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.ClosedField.type) :> Type.
+Check erefl : (_ : SplittingField.type) = (_ : Vector.type) :> Type.
+Check erefl : (_ : Finite.type) = (_ : GRing.Algebra.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : GRing.Field.type) = (_ : SplittingField.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : CountRing.Field.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.UnitRing.type) :> Type.
+Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : FinRing.Ring.type) :> Type.
+Check erefl : (_ : FinRing.UnitRing.type) = (_ : FinRing.Zmodule.type) :> Type.
+Check erefl : (_ : FinRing.Ring.type) = (_ : FinRing.Zmodule.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : Num.NumField.type) :> Type.
+Check erefl : (_ : GRing.ClosedField.type) = (_ : Num.NumField.type) :> Type.
+Check erefl : (_ : GRing.ComRing.type) = (_ : SplittingField.type) :> Type.
+Check erefl : (_ : GRing.ClosedField.type) = (_ : Num.NumDomain.type) :> Type.
+Check erefl : (_ : GRing.ComRing.type) = (_ : Num.RealDomain.type) :> Type.
+Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.Lmodule.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.RealField.type) :> Type.
+Check erefl : (_ : Num.RealClosedField.type) = (_ : Num.RealDomain.type) :> Type.
+Check erefl : (_ : Finite.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : FinRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.ClosedField.type) :> Type.
+Check erefl : (_ : FinGroup.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.RealClosedField.type) :> Type.
+Check erefl : (_ : Finite.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : FieldExt.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : GRing.Field.type) = (_ : GRing.Lalgebra.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : FinRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : GRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : CountRing.Field.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.ClosedField.type) :> Type.
+Check erefl : (_ : CountRing.Field.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : GRing.ClosedField.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : Vector.type) :> Type.
+Check erefl : (_ : GRing.Lalgebra.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.ComRing.type) :> Type.
+Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : CountRing.Zmodule.type) :> Type.
+Check erefl : (_ : FinRing.Ring.type) = (_ : FinRing.UnitRing.type) :> Type.
+Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : Countable.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : CountRing.Zmodule.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : SplittingField.type) :> Type.
+Check erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.Lalgebra.type) :> Type.
+Check erefl : (_ : FinRing.ComRing.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : FinRing.Lalgebra.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : GRing.DecidableField.type) = (_ : Num.ClosedField.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : GRing.ComRing.type) = (_ : Num.RealField.type) :> Type.
+Check erefl : (_ : GRing.ClosedField.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.ComRing.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : FinRing.UnitRing.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.ComRing.type) :> Type.
+Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : SplittingField.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : FinRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : CountRing.Field.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : GRing.Zmodule.type) = (_ : Vector.type) :> Type.
+Check erefl : (_ : CountRing.Field.type) = (_ : CountRing.Zmodule.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : FinRing.Field.type) :> Type.
+Check erefl : (_ : Falgebra.type) = (_ : GRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : FinRing.Algebra.type) = (_ : GRing.Algebra.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.Lalgebra.type) :> Type.
+Check erefl : (_ : GRing.Zmodule.type) = (_ : Num.NumDomain.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.Algebra.type) :> Type.
+Check erefl : (_ : FinGroup.type) = (_ : FinRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : Vector.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : FinRing.Zmodule.type) :> Type.
+Check erefl : (_ : Falgebra.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : Num.NumDomain.type) = (_ : Num.RealClosedField.type) :> Type.
+Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : FinRing.UnitRing.type) :> Type.
+Check erefl : (_ : CountRing.DecidableField.type) = (_ : CountRing.UnitRing.type) :> Type.
+Check erefl : (_ : FinGroup.type) = (_ : FinRing.Lmodule.type) :> Type.
+Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.UnitRing.type) :> Type.
+Check erefl : (_ : FieldExt.type) = (_ : GRing.Lmodule.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : FinGroup.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : CountRing.Field.type) = (_ : Finite.type) :> Type.
+Check erefl : (_ : FinGroup.type) = (_ : FinRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : GRing.Field.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : CountRing.Field.type) = (_ : CountRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : Num.ArchimedeanField.type) = (_ : Num.RealField.type) :> Type.
+Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.Algebra.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : FinRing.Lalgebra.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.Field.type) :> Type.
+Check erefl : (_ : GRing.UnitAlgebra.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : CountRing.Field.type) = (_ : FinRing.Field.type) :> Type.
+Check erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.Lmodule.type) :> Type.
+Check erefl : (_ : CountRing.Field.type) = (_ : CountRing.UnitRing.type) :> Type.
+Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : GRing.ComRing.type) = (_ : Vector.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : CountRing.Zmodule.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : FinGroup.type) = (_ : GRing.Algebra.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Zmodule.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.Ring.type) :> Type.
+Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.Lalgebra.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Lalgebra.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : GRing.Lalgebra.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : Finite.type) :> Type.
+Check erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.Lalgebra.type) :> Type.
+Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : GRing.ClosedField.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : GRing.Lalgebra.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : GRing.ComRing.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : CountRing.Field.type) = (_ : FinRing.Zmodule.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : Num.NumDomain.type) :> Type.
+Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : FinRing.UnitRing.type) :> Type.
+Check erefl : (_ : FinRing.UnitRing.type) = (_ : Finite.type) :> Type.
+Check erefl : (_ : FinGroup.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : FinRing.Lalgebra.type) = (_ : FinRing.UnitRing.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Lmodule.type) :> Type.
+Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : FinRing.Field.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Lmodule.type) :> Type.
+Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinGroup.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.UnitRing.type) :> Type.
+Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.ComRing.type) :> Type.
+Check erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Lalgebra.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : FinRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : GRing.DecidableField.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Field.type) :> Type.
+Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : FinGroup.type) = (_ : FinRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : GRing.Ring.type) = (_ : Vector.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : FinRing.Algebra.type) :> Type.
+Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : Finite.type) :> Type.
+Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.DecidableField.type) :> Type.
+Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : FinRing.Field.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Ring.type) :> Type.
+Check erefl : (_ : Num.ArchimedeanField.type) = (_ : Num.NumDomain.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : FinRing.Zmodule.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : GRing.ComRing.type) :> Type.
+Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : CountRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.Field.type) :> Type.
+Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.Zmodule.type) :> Type.
+Check erefl : (_ : CountRing.ClosedField.type) = (_ : Countable.type) :> Type.
+Check erefl : (_ : CountRing.DecidableField.type) = (_ : CountRing.Field.type) :> Type.
+Check erefl : (_ : CountRing.Field.type) = (_ : Equality.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : FinRing.ComRing.type) :> Type.
+Check erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : CountRing.Field.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : CountRing.Field.type) :> Type.
+Check erefl : (_ : GRing.Field.type) = (_ : Num.RealClosedField.type) :> Type.
+Check erefl : (_ : FinRing.Field.type) = (_ : FinRing.Ring.type) :> Type.
+Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Lalgebra.type) :> Type.
+Check erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.Ring.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : CountRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : FinRing.Field.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Algebra.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : CountRing.Zmodule.type) :> Type.
+Check erefl : (_ : CountRing.DecidableField.type) = (_ : Countable.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : Countable.type) :> Type.
+Check erefl : (_ : CountRing.DecidableField.type) = (_ : CountRing.Zmodule.type) :> Type.
+Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : FinRing.Ring.type) :> Type.
+Check erefl : (_ : FinGroup.type) = (_ : FinRing.ComRing.type) :> Type.
+Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.ComRing.type) :> Type.
+Check erefl : (_ : Falgebra.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : FinRing.Lalgebra.type) = (_ : FinRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.Lalgebra.type) :> Type.
+Check erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.Zmodule.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.Lmodule.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.ClosedField.type) :> Type.
+Check erefl : (_ : GRing.Lalgebra.type) = (_ : GRing.Lmodule.type) :> Type.
+Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.Lalgebra.type) :> Type.
+Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Zmodule.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Algebra.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : Countable.type) :> Type.
+Check erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.RealDomain.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.DecidableField.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : GRing.UnitRing.type) = (_ : Num.NumField.type) :> Type.
+Check erefl : (_ : GRing.DecidableField.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : GRing.ClosedField.type) = (_ : Num.ClosedField.type) :> Type.
+Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.ComRing.type) :> Type.
+Check erefl : (_ : FinGroup.type) = (_ : Finite.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : FinRing.UnitRing.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Algebra.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Lalgebra.type) :> Type.
+Check erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.Algebra.type) :> Type.
+Check erefl : (_ : FinRing.Ring.type) = (_ : Finite.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : Num.RealDomain.type) :> Type.
+Check erefl : (_ : Falgebra.type) = (_ : GRing.ComRing.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : GRing.Algebra.type) :> Type.
+Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : GRing.ComRing.type) = (_ : Num.RealClosedField.type) :> Type.
+Check erefl : (_ : GRing.IntegralDomain.type) = (_ : SplittingField.type) :> Type.
+Check erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : Falgebra.type) = (_ : GRing.Lalgebra.type) :> Type.
+Check erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.NumField.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : Falgebra.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.ClosedField.type) :> Type.
+Check erefl : (_ : GRing.ComRing.type) = (_ : Num.ClosedField.type) :> Type.
+Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.Field.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : Finite.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Lmodule.type) :> Type.
+Check erefl : (_ : FinRing.Lalgebra.type) = (_ : FinRing.Zmodule.type) :> Type.
+Check erefl : (_ : GRing.Lalgebra.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : GRing.UnitRing.type) = (_ : Num.NumDomain.type) :> Type.
+Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.Field.type) :> Type.
+Check erefl : (_ : Num.ClosedField.type) = (_ : Num.NumDomain.type) :> Type.
+Check erefl : (_ : FinRing.Field.type) = (_ : FinRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.ArchimedeanField.type) :> Type.
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : Equality.type) :> Type.
+Check erefl : (_ : Falgebra.type) = (_ : Vector.type) :> Type.
+Check erefl : (_ : GRing.Lmodule.type) = (_ : Vector.type) :> Type.
+Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : CountRing.UnitRing.type) :> Type.
+Check erefl : (_ : FinRing.Field.type) = (_ : FinRing.UnitRing.type) :> Type.
+Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : FinRing.ComRing.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : GRing.Ring.type) = (_ : SplittingField.type) :> Type.
+Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : FinGroup.type) = (_ : GRing.Lmodule.type) :> Type.
+Check erefl : (_ : CountRing.Field.type) = (_ : GRing.DecidableField.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : Countable.type) :> Type.
+Check erefl : (_ : FinGroup.type) = (_ : FinRing.Zmodule.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.UnitRing.type) :> Type.
+Check erefl : (_ : GRing.ClosedField.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : Num.NumDomain.type) = (_ : Num.NumField.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : FinRing.Ring.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : Num.ArchimedeanField.type) :> Type.
+Check erefl : (_ : FinGroup.type) = (_ : GRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.Field.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.DecidableField.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.Lalgebra.type) :> Type.
+Check erefl : (_ : FinRing.ComRing.type) = (_ : GRing.ComRing.type) :> Type.
+Check erefl : (_ : Falgebra.type) = (_ : GRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : GRing.ClosedField.type) :> Type.
+Check erefl : (_ : FieldExt.type) = (_ : Vector.type) :> Type.
+Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : Finite.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.Zmodule.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.DecidableField.type) :> Type.
+Check erefl : (_ : CountRing.Ring.type) = (_ : FinGroup.type) :> Type.
+Check erefl : (_ : Equality.type) = (_ : Num.RealClosedField.type) :> Type.
+Check erefl : (_ : GRing.Algebra.type) = (_ : Vector.type) :> Type.
+Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.ComRing.type) :> Type.
+Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.ComUnitRing.type) :> Type.
+Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : FinRing.Ring.type) :> Type.
+Check erefl : (_ : GRing.Ring.type) = (_ : GRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.Ring.type) :> Type.
+Check erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.ClosedField.type) :> Type.
+Check erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.Lmodule.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : GRing.Algebra.type) :> Type.
+Check erefl : (_ : FinRing.Algebra.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.RealDomain.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : FinRing.Algebra.type) :> Type.
+Check erefl : (_ : FinRing.Algebra.type) = (_ : GRing.Lalgebra.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : Num.RealClosedField.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : Equality.type) :> Type.
+Check erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.Lmodule.type) :> Type.
+Check erefl : (_ : FinRing.ComRing.type) = (_ : GRing.UnitRing.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : GRing.ClosedField.type) :> Type.
+Check erefl : (_ : Countable.type) = (_ : GRing.Ring.type) :> Type.
+Check erefl : (_ : Choice.type) = (_ : GRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.UnitAlgebra.type) :> Type.
+Check erefl : (_ : GRing.Zmodule.type) = (_ : Num.ArchimedeanField.type) :> Type.
+
+(* fix in ssrnum *)
+Check erefl : (_ : GRing.Field.type) = (_ : Num.NumDomain.type) :> Type.
+Check erefl : (_ : GRing.Field.type) = (_ : Num.RealDomain.type) :> Type.
+
+(* fix in countalg *)
+Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.IntegralDomain.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Lmodule.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Algebra.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Lalgebra.type) :> Type.
+
+(* fix in finalg *)
+Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Algebra.type) :> Type.
+Check erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.UnitRing.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Algebra.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Lalgebra.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Lmodule.type) :> Type.
+Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.ComRing.type) :> Type.
-- 
cgit v1.2.3