identifying missing joins

3 files changed, 766 insertions, 0 deletions

diff --git a/etc/utils/hierarchy_test.py b/etc/utils/hierarchy_test.py
new file mode 100644
index 0000000..bc90c55
--- /dev/null
+++ b/etc/utils/hierarchy_test.py
@@ -0,0 +1,46 @@
+#!/usr/bin/python
+# usage: hiearchy_test.py inputfile
+
+import pygraphviz as pgv
+import sys, argparse
+
+def children(G,n):
+    res = set()
+    new = set([n])
+    while new != set():
+        p = new.pop()
+        res.add(p)
+        new.update(set(G.successors(p)).difference(res))
+    return res
+
+def common_children(G):
+    result = set()
+    for x in G.nodes():
+        for y in G.nodes():
+            if children(G,x).intersection(children(G,y)) != set():
+                result.add((x,y))
+    return result
+
+def print_common_children_coq_check(G):
+    print("(** Generated by etc/utils/hierarchy_test.py *)")
+    print("From mathcomp Require Import all.")
+    for x in G.nodes():
+        if x.rfind("Lmod") >= 0 or x.rfind("Splitting") >= 0 or \
+           x.rfind("lgebra") >= 0 or x.rfind("FieldExt") >= 0 or \
+           x.rfind("Vector") >= 0:
+            print ("Local Notation \"" + x + ".type\" := (" + x + ".type _).")
+    print ("")
+    for (x, y) in common_children(G):
+        if x < y:
+            print ("Check erefl : (_ : " + x + ".type) = (_ : " + y + ".type) :> Type.")
+
+def main():
+    parser = argparse.ArgumentParser(description='Generate a check .v file \
+                 for mathcomp structure hiearchies')
+    parser.add_argument('dotfile', metavar='<dotfile>', nargs=1,
+                        help='a dotfile representing the hierarchy')
+    args = parser.parse_args()
+    print_common_children_coq_check(pgv.AGraph(args.dotfile[0]))
+
+if __name__ == "__main__":
+    main()
diff --git a/mathcomp/Make b/mathcomp/Make
index 147d5b1..27bf34f 100644
--- a/mathcomp/Make
+++ b/mathcomp/Make
@@ -87,6 +87,7 @@ ssreflect/ssrnat.v
 ssreflect/ssrnotations.v
 ssreflect/ssrmatching.v
 ssreflect/tuple.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
new file mode 100644
index 0000000..0085018
--- /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 *)
+Fail Check erefl : (_ : GRing.Field.type) = (_ : Num.NumDomain.type) :> Type.
+Fail Check erefl : (_ : GRing.Field.type) = (_ : Num.RealDomain.type) :> Type.
+
+(* fix in countalg *)
+Fail Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.IntegralDomain.type) :> Type.
+Fail Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Lmodule.type) :> Type.
+Fail Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Algebra.type) :> Type.
+Fail Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Lalgebra.type) :> Type.
+
+(* fix in finalg *)
+Fail Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Algebra.type) :> Type.
+Fail Check erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.UnitRing.type) :> Type.
+Fail Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Algebra.type) :> Type.
+Fail Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Lalgebra.type) :> Type.
+Fail Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Lmodule.type) :> Type.
+Fail Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.ComRing.type) :> Type.