Merge pull request #318 from CohenCyril/hierarchy_test

Least common childen

3 files changed, 1491 insertions, 719 deletions

diff --git a/mathcomp/algebra/finalg.v b/mathcomp/algebra/finalg.v
index ac3a74e..9c0025b 100644
--- a/mathcomp/algebra/finalg.v
+++ b/mathcomp/algebra/finalg.v
@@ -125,7 +125,9 @@ Coercion countType : type >-> Countable.type.
 Canonical countType.
 Coercion finType : type >-> Finite.type.
 Canonical finType.
+Coercion baseFinGroupType : type >-> FinGroup.base_type.
 Canonical baseFinGroupType.
+Coercion finGroupType : type >-> FinGroup.type.
 Canonical finGroupType.
 Coercion zmodType : type >-> GRing.Zmodule.type.
 Canonical zmodType.
@@ -645,13 +647,9 @@ Definition countComUnitRing_finComRingType :=
   @ComRing.Pack countComUnitRingType xclass.
 Definition countComUnitRing_finUnitRingType :=
   @UnitRing.Pack countComUnitRingType xclass.
-Definition unitRing_countComRingType :=
-  @CountRing.ComRing.Pack unitRingType xclass.
 Definition unitRing_finComRingType := @ComRing.Pack unitRingType xclass.
 Definition countUnitRing_finComRingType :=
   @ComRing.Pack countUnitRingType xclass.
-Definition comRing_countUnitRingType :=
-  @CountRing.UnitRing.Pack comRingType xclass.
 Definition comRing_finUnitRingType := @UnitRing.Pack comRingType xclass.
 Definition countComRing_finUnitRingType :=
   @UnitRing.Pack countComRingType xclass.
@@ -720,10 +718,8 @@ Canonical countComUnitRing_finZmodType.
 Canonical countComUnitRing_finRingType.
 Canonical countComUnitRing_finComRingType.
 Canonical countComUnitRing_finUnitRingType.
-Canonical unitRing_countComRingType.
 Canonical unitRing_finComRingType.
 Canonical countUnitRing_finComRingType.
-Canonical comRing_countUnitRingType.
 Canonical comRing_finUnitRingType.
 Canonical countComRing_finUnitRingType.
 Canonical finComRing_finUnitRingType.
@@ -1231,7 +1227,6 @@ Definition lalg_finZmodType := @Zmodule.Pack lalgType xclass.
 Definition lalg_finLmodType := @Lmodule.Pack R phR lalgType xclass.
 Definition lalg_countRingType := @CountRing.Ring.Pack lalgType xclass.
 Definition lalg_finRingType := @Ring.Pack lalgType xclass.
-Definition lmod_ringType := @GRing.Ring.Pack lmodType xclass.
 Definition lmod_countRingType := @CountRing.Ring.Pack lmodType xclass.
 Definition lmod_finRingType := @Ring.Pack lmodType xclass.
 Definition finLmod_ringType := @GRing.Ring.Pack finLmodType xclass.
@@ -1285,7 +1280,6 @@ Canonical lalg_finZmodType.
 Canonical lalg_finLmodType.
 Canonical lalg_countRingType.
 Canonical lalg_finRingType.
-Canonical lmod_ringType.
 Canonical lmod_countRingType.
 Canonical lmod_finRingType.
 Canonical finLmod_ringType.
diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v
index 9ac5236..a51fe9c 100644
--- a/mathcomp/solvable/extremal.v
+++ b/mathcomp/solvable/extremal.v
@@ -1533,7 +1533,8 @@ Canonical extremal_group_countType := CountType _ extremal_group_countMixin.
 Lemma bound_extremal_groups (c : extremal_group_type) : pickle c < 6.
 Proof. by case: c. Qed.
 Definition extremal_group_finMixin := Finite.CountMixin bound_extremal_groups.
-Canonical extremal_group_finType := FinType _ extremal_group_finMixin.
+Canonical extremal_group_finType :=
+  FinType extremal_group_type extremal_group_finMixin.
 
 Definition extremal_class (A : {set gT}) :=
   let m := #|A| in let p := pdiv m in let n := logn p m in
diff --git a/mathcomp/test_suite/hierarchy_test.v b/mathcomp/test_suite/hierarchy_test.v
index e806362..5ea8980 100644
--- a/mathcomp/test_suite/hierarchy_test.v
+++ b/mathcomp/test_suite/hierarchy_test.v
@@ -1,713 +1,1490 @@
 (** 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 _).
 
-Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : GRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : Countable.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : GRing.DecidableField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.UnitRing.type) = (_ : Num.ArchimedeanField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Algebra.type) = (_ : GRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinGroup.type) = (_ : Finite.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FieldExt.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : Countable.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.Algebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.DecidableField.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.DecidableField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Falgebra.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.DecidableField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Lmodule.type) = (_ : FinRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : FinGroup.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Field.type) = (_ : GRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : Countable.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : FinRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : Countable.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : Finite.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : Countable.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Field.type) = (_ : Vector.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : SplittingField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : FinRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : Num.RealClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Num.ArchimedeanField.type) = (_ : Num.NumDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.UnitAlgebra.type) = (_ : Finite.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : Finite.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Field.type) = (_ : Num.RealClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Zmodule.type) = (_ : Num.RealDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FieldExt.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FieldExt.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Falgebra.type) = (_ : GRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : Num.NumDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Zmodule.type) = (_ : Finite.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinGroup.type) = (_ : GRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FieldExt.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Algebra.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : CountRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinGroup.type) = (_ : FinRing.Algebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : GRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Falgebra.type) = (_ : FieldExt.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : GRing.ClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.UnitRing.type) = (_ : Vector.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : FinRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Algebra.type) = (_ : Vector.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : Falgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : FinRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : Finite.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : SplittingField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Field.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Field.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.IntegralDomain.type) = (_ : FinRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : Num.RealField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : FinRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Algebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.ClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : FinRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Field.type) = (_ : Num.NumDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.Algebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinGroup.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : FinRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.IntegralDomain.type) = (_ : FinRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : FinRing.Algebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : CountRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : Finite.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Zmodule.type) = (_ : Vector.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Finite.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : Num.RealDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.Algebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : Num.NumField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Lmodule.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Ring.type) = (_ : Num.RealDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.RealDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : FinRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : CountRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : FinRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : Num.NumField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinGroup.type) = (_ : GRing.Algebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Num.RealClosedField.type) = (_ : Num.RealField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : SplittingField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : FinGroup.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Algebra.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Num.ArchimedeanField.type) = (_ : Num.RealField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.UnitRing.type) = (_ : SplittingField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.RealField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : Finite.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.UnitRing.type) = (_ : Num.NumDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : SplittingField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Lalgebra.type) = (_ : Vector.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : Num.RealField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Algebra.type) = (_ : GRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Field.type) = (_ : Num.ClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : FinRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.Algebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : FinRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Finite.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : Num.ClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : FinRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinGroup.type) = (_ : FinRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Ring.type) = (_ : Num.ArchimedeanField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.ArchimedeanField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ClosedField.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ClosedField.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ClosedField.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Falgebra.type) = (_ : Vector.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : FinRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : CountRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Lmodule.type) = (_ : Finite.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Num.NumDomain.type) = (_ : Num.RealDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.NumField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Field.type) = (_ : SplittingField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : FinRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinGroup.type) = (_ : FinRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ClosedField.type) = (_ : Num.NumDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Falgebra.type) = (_ : SplittingField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Algebra.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FieldExt.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : Num.ArchimedeanField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : FinRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinGroup.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : FinRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Ring.type) = (_ : Num.NumDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.ClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.NumDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Falgebra.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Num.NumDomain.type) = (_ : Num.RealClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Algebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : Vector.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : FinGroup.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Lalgebra.type) = (_ : GRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.ClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.DecidableField.type) = (_ : Num.ClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : FinRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.ClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : FinRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.ClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Falgebra.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : FieldExt.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.ClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : GRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : GRing.Algebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Lmodule.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : Equality.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Ring.type) = (_ : Num.ClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : CountRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.ClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Zmodule.type) = (_ : Num.NumDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : GRing.DecidableField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.DecidableField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : CountRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : FinRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : FinRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Finite.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : CountRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Field.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : FinRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.Algebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : GRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.DecidableField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : FinRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : FinRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : Countable.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : GRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : FinRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.UnitAlgebra.type) = (_ : FinRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.DecidableField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : FinRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinGroup.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : FinRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Field.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Field.type) = (_ : GRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Num.ClosedField.type) = (_ : Num.NumDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : SplittingField.type) = (_ : Vector.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ClosedField.type) = (_ : GRing.DecidableField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinGroup.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Lalgebra.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Algebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : Finite.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : FinRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : Countable.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : FinGroup.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : Falgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Ring.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : CountRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : Equality.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.DecidableField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : Equality.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Finite.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.DecidableField.type) = (_ : Num.NumField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Field.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.UnitRing.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Ring.type) = (_ : Num.RealField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ClosedField.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : Finite.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.RealField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinGroup.type) = (_ : GRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Finite.type) = (_ : GRing.Algebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : Num.NumDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinGroup.type) = (_ : FinRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : FinGroup.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinGroup.type) = (_ : GRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.DecidableField.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : FinRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : Num.NumDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinGroup.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : Equality.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Ring.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Falgebra.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : GRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Lmodule.type) = (_ : Vector.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : CountRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Num.NumField.type) = (_ : Num.RealClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Field.type) = (_ : Num.RealField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ClosedField.type) = (_ : Num.ClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Lmodule.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Lalgebra.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Zmodule.type) = (_ : Num.ArchimedeanField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Algebra.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Algebra.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : Finite.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Zmodule.type) = (_ : Num.ClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Lmodule.type) = (_ : FinRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : FinRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : Finite.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.Algebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.NumDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Lmodule.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.UnitAlgebra.type) = (_ : FinRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Algebra.type) = (_ : GRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : CountRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.UnitRing.type) = (_ : Num.RealField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ClosedField.type) = (_ : Num.NumField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : GRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : FinGroup.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : Num.RealClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Algebra.type) = (_ : SplittingField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinGroup.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.DecidableField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : Num.RealDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : FinRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : CountRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : CountRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : GRing.Algebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : GRing.ClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Ring.type) = (_ : Num.NumField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.NumField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Field.type) = (_ : Finite.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.ClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.UnitAlgebra.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : Num.ClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : Equality.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.ArchimedeanField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : Num.RealField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Num.NumDomain.type) = (_ : Num.NumField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Field.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Zmodule.type) = (_ : Num.NumField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : Vector.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : FinRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : GRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Algebra.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Field.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : FinRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : Equality.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : Finite.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.RealDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Finite.type) = (_ : GRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.DecidableField.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.UnitRing.type) = (_ : Num.RealClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinGroup.type) = (_ : FinRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : FinRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.DecidableField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.DecidableField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : FinRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Lmodule.type) = (_ : SplittingField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Num.ClosedField.type) = (_ : Num.NumField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.ClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.DecidableField.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.DecidableField.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : CountRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : FieldExt.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : FinGroup.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : Finite.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : Equality.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.DecidableField.type) = (_ : Num.NumDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Ring.type) = (_ : SplittingField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : SplittingField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FieldExt.type) = (_ : Vector.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.DecidableField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : CountRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : CountRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : CountRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Field.type) = (_ : Num.ArchimedeanField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : FinRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FieldExt.type) = (_ : GRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : FinRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinGroup.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Field.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Finite.type) = (_ : GRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : Num.NumField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Falgebra.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : FinRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.DecidableField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : Finite.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Field.type) = (_ : FinRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.IntegralDomain.type) = (_ : FinRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : CountRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : CountRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Finite.type) = (_ : GRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Lalgebra.type) = (_ : SplittingField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : Finite.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : FinRing.Algebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinGroup.type) = (_ : FinRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : Countable.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : CountRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.ClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : FinRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ClosedField.type) = (_ : GRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.Algebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Field.type) = (_ : FinRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : Vector.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FieldExt.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : FinRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : Num.ClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : FinRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Ring.type) = (_ : Num.RealClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.RealClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.UnitAlgebra.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.UnitRing.type) = (_ : Num.ClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Ring.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : FinRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Lalgebra.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : Equality.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.ClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Lmodule.type) = (_ : FinRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Num.RealDomain.type) = (_ : Num.RealField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FieldExt.type) = (_ : GRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : GRing.DecidableField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : FinRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Field.type) = (_ : Num.NumField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Zmodule.type) = (_ : SplittingField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Algebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Num.ArchimedeanField.type) = (_ : Num.NumField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : Countable.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Field.type) = (_ : FinRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinGroup.type) = (_ : FinRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : Num.RealDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Field.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : Countable.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Field.type) = (_ : Num.RealDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Zmodule.type) = (_ : Num.RealClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : FinRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : Equality.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinGroup.type) = (_ : FinRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Falgebra.type) = (_ : GRing.Algebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Algebra.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : Vector.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.DecidableField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComUnitRing.type) = (_ : Finite.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.IntegralDomain.type) = (_ : Finite.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Falgebra.type) = (_ : GRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.UnitRing.type) = (_ : Num.NumField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.RealClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FieldExt.type) = (_ : GRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ClosedField.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : Equality.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : GRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComRing.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : FinRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.DecidableField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : FinRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Finite.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Finite.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Ring.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : FinRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : FinRing.Algebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Lmodule.type) = (_ : FinRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.DecidableField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Algebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Num.NumDomain.type) = (_ : Num.RealField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : FinRing.Lmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : FinRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : FinGroup.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : Num.ArchimedeanField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinGroup.type) = (_ : FinRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Finite.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Num.NumField.type) = (_ : Num.RealField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Field.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Field.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : Finite.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinGroup.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinGroup.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : Finite.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ClosedField.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Num.ArchimedeanField.type) = (_ : Num.RealDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Lalgebra.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : CountRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.UnitAlgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Num.RealClosedField.type) = (_ : Num.RealDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Ring.type) = (_ : FinRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : Equality.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Field.type) = (_ : GRing.Lalgebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.UnitAlgebra.type) = (_ : Vector.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FieldExt.type) = (_ : SplittingField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Field.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinGroup.type) = (_ : FinRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Ring.type) = (_ : Vector.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.IntegralDomain.type) = (_ : Vector.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.UnitRing.type) = (_ : Num.RealDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Falgebra.type) = (_ : GRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : GRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Field.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Algebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : FinRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Num.NumField.type) = (_ : Num.RealDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : Num.ArchimedeanField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.UnitAlgebra.type) = (_ : SplittingField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FieldExt.type) = (_ : GRing.Algebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : CountRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : CountRing.DecidableField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinGroup.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : GRing.UnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Falgebra.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Falgebra.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : GRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FinRing.ComRing.type) = (_ : GRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : FieldExt.type) = (_ : GRing.Zmodule.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.ClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : GRing.Zmodule.type) = (_ : Num.RealField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : FinRing.Ring.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Choice.type) = (_ : CountRing.ClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Algebra.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Countable.type) = (_ : GRing.ComRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : GRing.ComUnitRing.type) :> Type. Abort.
-Goal False. have := erefl : (_ : Equality.type) = (_ : Num.RealClosedField.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.Field.type) = (_ : CountRing.IntegralDomain.type) :> Type. Abort.
-Goal False. have := erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.IntegralDomain.type) :> Type. Abort.
+(* `check_join t1 t2 tjoin` assert that the join of `t1` and `t2` is `tjoin`. *)
+Tactic Notation "check_join"
+       open_constr(t1) open_constr(t2) open_constr(tjoin) :=
+  let T1 := open_constr:(_ : t1) in
+  let T2 := open_constr:(_ : t2) in
+  match tt with
+    | _ => unify ((id : t1 -> Type) T1) ((id : t2 -> Type) T2)
+    | _ => fail "There is no join of" t1 "and" t2
+  end;
+  let Tjoin :=
+    lazymatch T1 with
+      | _ (_ ?Tjoin) => constr: (Tjoin)
+      | _ ?Tjoin => constr: (Tjoin)
+      | ?Tjoin => constr: (Tjoin)
+    end
+  in
+  is_evar Tjoin;
+  let tjoin' := type of Tjoin in
+  lazymatch tjoin' with
+    | tjoin => lazymatch tjoin with
+                 | tjoin' => idtac
+                 | _ => idtac tjoin'
+               end
+    | _ => fail "The join of" t1 "and" t2 "is" tjoin'
+                "but is expected to be" tjoin
+  end.
+
+Local Notation "Falgebra.type" := (Falgebra.type _) (only parsing).
+Local Notation "FieldExt.type" := (FieldExt.type _) (only parsing).
+Local Notation "FinRing.Algebra.type" := (FinRing.Algebra.type _) (only parsing).
+Local Notation "FinRing.Lalgebra.type" := (FinRing.Lalgebra.type _) (only parsing).
+Local Notation "FinRing.Lmodule.type" := (FinRing.Lmodule.type _) (only parsing).
+Local Notation "FinRing.UnitAlgebra.type" := (FinRing.UnitAlgebra.type _) (only parsing).
+Local Notation "GRing.Algebra.type" := (GRing.Algebra.type _) (only parsing).
+Local Notation "GRing.Lalgebra.type" := (GRing.Lalgebra.type _) (only parsing).
+Local Notation "GRing.Lmodule.type" := (GRing.Lmodule.type _) (only parsing).
+Local Notation "GRing.UnitAlgebra.type" := (GRing.UnitAlgebra.type _) (only parsing).
+Local Notation "SplittingField.type" := (SplittingField.type _) (only parsing).
+Local Notation "Vector.type" := (Vector.type _) (only parsing).
+
+Goal False.
+check_join Choice.type Choice.type Choice.type.
+check_join Choice.type CountRing.ClosedField.type CountRing.ClosedField.type.
+check_join Choice.type CountRing.ComRing.type CountRing.ComRing.type.
+check_join Choice.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type.
+check_join Choice.type CountRing.DecidableField.type CountRing.DecidableField.type.
+check_join Choice.type CountRing.Field.type CountRing.Field.type.
+check_join Choice.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type.
+check_join Choice.type CountRing.Ring.type CountRing.Ring.type.
+check_join Choice.type CountRing.UnitRing.type CountRing.UnitRing.type.
+check_join Choice.type CountRing.Zmodule.type CountRing.Zmodule.type.
+check_join Choice.type Countable.type Countable.type.
+check_join Choice.type Equality.type Choice.type.
+check_join Choice.type Falgebra.type Falgebra.type.
+check_join Choice.type FieldExt.type FieldExt.type.
+check_join Choice.type FinGroup.type FinGroup.type.
+check_join Choice.type FinRing.Algebra.type FinRing.Algebra.type.
+check_join Choice.type FinRing.ComRing.type FinRing.ComRing.type.
+check_join Choice.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join Choice.type FinRing.Field.type FinRing.Field.type.
+check_join Choice.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join Choice.type FinRing.Lalgebra.type FinRing.Lalgebra.type.
+check_join Choice.type FinRing.Lmodule.type FinRing.Lmodule.type.
+check_join Choice.type FinRing.Ring.type FinRing.Ring.type.
+check_join Choice.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join Choice.type FinRing.UnitRing.type FinRing.UnitRing.type.
+check_join Choice.type FinRing.Zmodule.type FinRing.Zmodule.type.
+check_join Choice.type Finite.type Finite.type.
+check_join Choice.type GRing.Algebra.type GRing.Algebra.type.
+check_join Choice.type GRing.ClosedField.type GRing.ClosedField.type.
+check_join Choice.type GRing.ComRing.type GRing.ComRing.type.
+check_join Choice.type GRing.ComUnitRing.type GRing.ComUnitRing.type.
+check_join Choice.type GRing.DecidableField.type GRing.DecidableField.type.
+check_join Choice.type GRing.Field.type GRing.Field.type.
+check_join Choice.type GRing.IntegralDomain.type GRing.IntegralDomain.type.
+check_join Choice.type GRing.Lalgebra.type GRing.Lalgebra.type.
+check_join Choice.type GRing.Lmodule.type GRing.Lmodule.type.
+check_join Choice.type GRing.Ring.type GRing.Ring.type.
+check_join Choice.type GRing.UnitAlgebra.type GRing.UnitAlgebra.type.
+check_join Choice.type GRing.UnitRing.type GRing.UnitRing.type.
+check_join Choice.type GRing.Zmodule.type GRing.Zmodule.type.
+check_join Choice.type Num.ArchimedeanField.type Num.ArchimedeanField.type.
+check_join Choice.type Num.ClosedField.type Num.ClosedField.type.
+check_join Choice.type Num.NumDomain.type Num.NumDomain.type.
+check_join Choice.type Num.NumField.type Num.NumField.type.
+check_join Choice.type Num.RealClosedField.type Num.RealClosedField.type.
+check_join Choice.type Num.RealDomain.type Num.RealDomain.type.
+check_join Choice.type Num.RealField.type Num.RealField.type.
+check_join Choice.type SplittingField.type SplittingField.type.
+check_join Choice.type Vector.type Vector.type.
+check_join CountRing.ClosedField.type Choice.type CountRing.ClosedField.type.
+check_join CountRing.ClosedField.type CountRing.ClosedField.type CountRing.ClosedField.type.
+check_join CountRing.ClosedField.type CountRing.ComRing.type CountRing.ClosedField.type.
+check_join CountRing.ClosedField.type CountRing.ComUnitRing.type CountRing.ClosedField.type.
+check_join CountRing.ClosedField.type CountRing.DecidableField.type CountRing.ClosedField.type.
+check_join CountRing.ClosedField.type CountRing.Field.type CountRing.ClosedField.type.
+check_join CountRing.ClosedField.type CountRing.IntegralDomain.type CountRing.ClosedField.type.
+check_join CountRing.ClosedField.type CountRing.Ring.type CountRing.ClosedField.type.
+check_join CountRing.ClosedField.type CountRing.UnitRing.type CountRing.ClosedField.type.
+check_join CountRing.ClosedField.type CountRing.Zmodule.type CountRing.ClosedField.type.
+check_join CountRing.ClosedField.type Countable.type CountRing.ClosedField.type.
+check_join CountRing.ClosedField.type Equality.type CountRing.ClosedField.type.
+check_join CountRing.ClosedField.type GRing.ClosedField.type CountRing.ClosedField.type.
+check_join CountRing.ClosedField.type GRing.ComRing.type CountRing.ClosedField.type.
+check_join CountRing.ClosedField.type GRing.ComUnitRing.type CountRing.ClosedField.type.
+check_join CountRing.ClosedField.type GRing.DecidableField.type CountRing.ClosedField.type.
+check_join CountRing.ClosedField.type GRing.Field.type CountRing.ClosedField.type.
+check_join CountRing.ClosedField.type GRing.IntegralDomain.type CountRing.ClosedField.type.
+check_join CountRing.ClosedField.type GRing.Ring.type CountRing.ClosedField.type.
+check_join CountRing.ClosedField.type GRing.UnitRing.type CountRing.ClosedField.type.
+check_join CountRing.ClosedField.type GRing.Zmodule.type CountRing.ClosedField.type.
+check_join CountRing.ComRing.type Choice.type CountRing.ComRing.type.
+check_join CountRing.ComRing.type CountRing.ClosedField.type CountRing.ClosedField.type.
+check_join CountRing.ComRing.type CountRing.ComRing.type CountRing.ComRing.type.
+check_join CountRing.ComRing.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type.
+check_join CountRing.ComRing.type CountRing.DecidableField.type CountRing.DecidableField.type.
+check_join CountRing.ComRing.type CountRing.Field.type CountRing.Field.type.
+check_join CountRing.ComRing.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type.
+check_join CountRing.ComRing.type CountRing.Ring.type CountRing.ComRing.type.
+check_join CountRing.ComRing.type CountRing.UnitRing.type CountRing.ComUnitRing.type.
+check_join CountRing.ComRing.type CountRing.Zmodule.type CountRing.ComRing.type.
+check_join CountRing.ComRing.type Countable.type CountRing.ComRing.type.
+check_join CountRing.ComRing.type Equality.type CountRing.ComRing.type.
+check_join CountRing.ComRing.type FinGroup.type FinRing.ComRing.type.
+check_join CountRing.ComRing.type FinRing.ComRing.type FinRing.ComRing.type.
+check_join CountRing.ComRing.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join CountRing.ComRing.type FinRing.Field.type FinRing.Field.type.
+check_join CountRing.ComRing.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join CountRing.ComRing.type FinRing.Ring.type FinRing.ComRing.type.
+check_join CountRing.ComRing.type FinRing.UnitRing.type FinRing.ComUnitRing.type.
+check_join CountRing.ComRing.type FinRing.Zmodule.type FinRing.ComRing.type.
+check_join CountRing.ComRing.type Finite.type FinRing.ComRing.type.
+check_join CountRing.ComRing.type GRing.ClosedField.type CountRing.ClosedField.type.
+check_join CountRing.ComRing.type GRing.ComRing.type CountRing.ComRing.type.
+check_join CountRing.ComRing.type GRing.ComUnitRing.type CountRing.ComUnitRing.type.
+check_join CountRing.ComRing.type GRing.DecidableField.type CountRing.DecidableField.type.
+check_join CountRing.ComRing.type GRing.Field.type CountRing.Field.type.
+check_join CountRing.ComRing.type GRing.IntegralDomain.type CountRing.IntegralDomain.type.
+check_join CountRing.ComRing.type GRing.Ring.type CountRing.ComRing.type.
+check_join CountRing.ComRing.type GRing.UnitRing.type CountRing.ComUnitRing.type.
+check_join CountRing.ComRing.type GRing.Zmodule.type CountRing.ComRing.type.
+check_join CountRing.ComUnitRing.type Choice.type CountRing.ComUnitRing.type.
+check_join CountRing.ComUnitRing.type CountRing.ClosedField.type CountRing.ClosedField.type.
+check_join CountRing.ComUnitRing.type CountRing.ComRing.type CountRing.ComUnitRing.type.
+check_join CountRing.ComUnitRing.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type.
+check_join CountRing.ComUnitRing.type CountRing.DecidableField.type CountRing.DecidableField.type.
+check_join CountRing.ComUnitRing.type CountRing.Field.type CountRing.Field.type.
+check_join CountRing.ComUnitRing.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type.
+check_join CountRing.ComUnitRing.type CountRing.Ring.type CountRing.ComUnitRing.type.
+check_join CountRing.ComUnitRing.type CountRing.UnitRing.type CountRing.ComUnitRing.type.
+check_join CountRing.ComUnitRing.type CountRing.Zmodule.type CountRing.ComUnitRing.type.
+check_join CountRing.ComUnitRing.type Countable.type CountRing.ComUnitRing.type.
+check_join CountRing.ComUnitRing.type Equality.type CountRing.ComUnitRing.type.
+check_join CountRing.ComUnitRing.type FinGroup.type FinRing.ComUnitRing.type.
+check_join CountRing.ComUnitRing.type FinRing.ComRing.type FinRing.ComUnitRing.type.
+check_join CountRing.ComUnitRing.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join CountRing.ComUnitRing.type FinRing.Field.type FinRing.Field.type.
+check_join CountRing.ComUnitRing.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join CountRing.ComUnitRing.type FinRing.Ring.type FinRing.ComUnitRing.type.
+check_join CountRing.ComUnitRing.type FinRing.UnitRing.type FinRing.ComUnitRing.type.
+check_join CountRing.ComUnitRing.type FinRing.Zmodule.type FinRing.ComUnitRing.type.
+check_join CountRing.ComUnitRing.type Finite.type FinRing.ComUnitRing.type.
+check_join CountRing.ComUnitRing.type GRing.ClosedField.type CountRing.ClosedField.type.
+check_join CountRing.ComUnitRing.type GRing.ComRing.type CountRing.ComUnitRing.type.
+check_join CountRing.ComUnitRing.type GRing.ComUnitRing.type CountRing.ComUnitRing.type.
+check_join CountRing.ComUnitRing.type GRing.DecidableField.type CountRing.DecidableField.type.
+check_join CountRing.ComUnitRing.type GRing.Field.type CountRing.Field.type.
+check_join CountRing.ComUnitRing.type GRing.IntegralDomain.type CountRing.IntegralDomain.type.
+check_join CountRing.ComUnitRing.type GRing.Ring.type CountRing.ComUnitRing.type.
+check_join CountRing.ComUnitRing.type GRing.UnitRing.type CountRing.ComUnitRing.type.
+check_join CountRing.ComUnitRing.type GRing.Zmodule.type CountRing.ComUnitRing.type.
+check_join CountRing.DecidableField.type Choice.type CountRing.DecidableField.type.
+check_join CountRing.DecidableField.type CountRing.ClosedField.type CountRing.ClosedField.type.
+check_join CountRing.DecidableField.type CountRing.ComRing.type CountRing.DecidableField.type.
+check_join CountRing.DecidableField.type CountRing.ComUnitRing.type CountRing.DecidableField.type.
+check_join CountRing.DecidableField.type CountRing.DecidableField.type CountRing.DecidableField.type.
+check_join CountRing.DecidableField.type CountRing.Field.type CountRing.DecidableField.type.
+check_join CountRing.DecidableField.type CountRing.IntegralDomain.type CountRing.DecidableField.type.
+check_join CountRing.DecidableField.type CountRing.Ring.type CountRing.DecidableField.type.
+check_join CountRing.DecidableField.type CountRing.UnitRing.type CountRing.DecidableField.type.
+check_join CountRing.DecidableField.type CountRing.Zmodule.type CountRing.DecidableField.type.
+check_join CountRing.DecidableField.type Countable.type CountRing.DecidableField.type.
+check_join CountRing.DecidableField.type Equality.type CountRing.DecidableField.type.
+check_join CountRing.DecidableField.type GRing.ClosedField.type CountRing.ClosedField.type.
+check_join CountRing.DecidableField.type GRing.ComRing.type CountRing.DecidableField.type.
+check_join CountRing.DecidableField.type GRing.ComUnitRing.type CountRing.DecidableField.type.
+check_join CountRing.DecidableField.type GRing.DecidableField.type CountRing.DecidableField.type.
+check_join CountRing.DecidableField.type GRing.Field.type CountRing.DecidableField.type.
+check_join CountRing.DecidableField.type GRing.IntegralDomain.type CountRing.DecidableField.type.
+check_join CountRing.DecidableField.type GRing.Ring.type CountRing.DecidableField.type.
+check_join CountRing.DecidableField.type GRing.UnitRing.type CountRing.DecidableField.type.
+check_join CountRing.DecidableField.type GRing.Zmodule.type CountRing.DecidableField.type.
+check_join CountRing.Field.type Choice.type CountRing.Field.type.
+check_join CountRing.Field.type CountRing.ClosedField.type CountRing.ClosedField.type.
+check_join CountRing.Field.type CountRing.ComRing.type CountRing.Field.type.
+check_join CountRing.Field.type CountRing.ComUnitRing.type CountRing.Field.type.
+check_join CountRing.Field.type CountRing.DecidableField.type CountRing.DecidableField.type.
+check_join CountRing.Field.type CountRing.Field.type CountRing.Field.type.
+check_join CountRing.Field.type CountRing.IntegralDomain.type CountRing.Field.type.
+check_join CountRing.Field.type CountRing.Ring.type CountRing.Field.type.
+check_join CountRing.Field.type CountRing.UnitRing.type CountRing.Field.type.
+check_join CountRing.Field.type CountRing.Zmodule.type CountRing.Field.type.
+check_join CountRing.Field.type Countable.type CountRing.Field.type.
+check_join CountRing.Field.type Equality.type CountRing.Field.type.
+check_join CountRing.Field.type FinGroup.type FinRing.Field.type.
+check_join CountRing.Field.type FinRing.ComRing.type FinRing.Field.type.
+check_join CountRing.Field.type FinRing.ComUnitRing.type FinRing.Field.type.
+check_join CountRing.Field.type FinRing.Field.type FinRing.Field.type.
+check_join CountRing.Field.type FinRing.IntegralDomain.type FinRing.Field.type.
+check_join CountRing.Field.type FinRing.Ring.type FinRing.Field.type.
+check_join CountRing.Field.type FinRing.UnitRing.type FinRing.Field.type.
+check_join CountRing.Field.type FinRing.Zmodule.type FinRing.Field.type.
+check_join CountRing.Field.type Finite.type FinRing.Field.type.
+check_join CountRing.Field.type GRing.ClosedField.type CountRing.ClosedField.type.
+check_join CountRing.Field.type GRing.ComRing.type CountRing.Field.type.
+check_join CountRing.Field.type GRing.ComUnitRing.type CountRing.Field.type.
+check_join CountRing.Field.type GRing.DecidableField.type CountRing.DecidableField.type.
+check_join CountRing.Field.type GRing.Field.type CountRing.Field.type.
+check_join CountRing.Field.type GRing.IntegralDomain.type CountRing.Field.type.
+check_join CountRing.Field.type GRing.Ring.type CountRing.Field.type.
+check_join CountRing.Field.type GRing.UnitRing.type CountRing.Field.type.
+check_join CountRing.Field.type GRing.Zmodule.type CountRing.Field.type.
+check_join CountRing.IntegralDomain.type Choice.type CountRing.IntegralDomain.type.
+check_join CountRing.IntegralDomain.type CountRing.ClosedField.type CountRing.ClosedField.type.
+check_join CountRing.IntegralDomain.type CountRing.ComRing.type CountRing.IntegralDomain.type.
+check_join CountRing.IntegralDomain.type CountRing.ComUnitRing.type CountRing.IntegralDomain.type.
+check_join CountRing.IntegralDomain.type CountRing.DecidableField.type CountRing.DecidableField.type.
+check_join CountRing.IntegralDomain.type CountRing.Field.type CountRing.Field.type.
+check_join CountRing.IntegralDomain.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type.
+check_join CountRing.IntegralDomain.type CountRing.Ring.type CountRing.IntegralDomain.type.
+check_join CountRing.IntegralDomain.type CountRing.UnitRing.type CountRing.IntegralDomain.type.
+check_join CountRing.IntegralDomain.type CountRing.Zmodule.type CountRing.IntegralDomain.type.
+check_join CountRing.IntegralDomain.type Countable.type CountRing.IntegralDomain.type.
+check_join CountRing.IntegralDomain.type Equality.type CountRing.IntegralDomain.type.
+check_join CountRing.IntegralDomain.type FinGroup.type FinRing.IntegralDomain.type.
+check_join CountRing.IntegralDomain.type FinRing.ComRing.type FinRing.IntegralDomain.type.
+check_join CountRing.IntegralDomain.type FinRing.ComUnitRing.type FinRing.IntegralDomain.type.
+check_join CountRing.IntegralDomain.type FinRing.Field.type FinRing.Field.type.
+check_join CountRing.IntegralDomain.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join CountRing.IntegralDomain.type FinRing.Ring.type FinRing.IntegralDomain.type.
+check_join CountRing.IntegralDomain.type FinRing.UnitRing.type FinRing.IntegralDomain.type.
+check_join CountRing.IntegralDomain.type FinRing.Zmodule.type FinRing.IntegralDomain.type.
+check_join CountRing.IntegralDomain.type Finite.type FinRing.IntegralDomain.type.
+check_join CountRing.IntegralDomain.type GRing.ClosedField.type CountRing.ClosedField.type.
+check_join CountRing.IntegralDomain.type GRing.ComRing.type CountRing.IntegralDomain.type.
+check_join CountRing.IntegralDomain.type GRing.ComUnitRing.type CountRing.IntegralDomain.type.
+check_join CountRing.IntegralDomain.type GRing.DecidableField.type CountRing.DecidableField.type.
+check_join CountRing.IntegralDomain.type GRing.Field.type CountRing.Field.type.
+check_join CountRing.IntegralDomain.type GRing.IntegralDomain.type CountRing.IntegralDomain.type.
+check_join CountRing.IntegralDomain.type GRing.Ring.type CountRing.IntegralDomain.type.
+check_join CountRing.IntegralDomain.type GRing.UnitRing.type CountRing.IntegralDomain.type.
+check_join CountRing.IntegralDomain.type GRing.Zmodule.type CountRing.IntegralDomain.type.
+check_join CountRing.Ring.type Choice.type CountRing.Ring.type.
+check_join CountRing.Ring.type CountRing.ClosedField.type CountRing.ClosedField.type.
+check_join CountRing.Ring.type CountRing.ComRing.type CountRing.ComRing.type.
+check_join CountRing.Ring.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type.
+check_join CountRing.Ring.type CountRing.DecidableField.type CountRing.DecidableField.type.
+check_join CountRing.Ring.type CountRing.Field.type CountRing.Field.type.
+check_join CountRing.Ring.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type.
+check_join CountRing.Ring.type CountRing.Ring.type CountRing.Ring.type.
+check_join CountRing.Ring.type CountRing.UnitRing.type CountRing.UnitRing.type.
+check_join CountRing.Ring.type CountRing.Zmodule.type CountRing.Ring.type.
+check_join CountRing.Ring.type Countable.type CountRing.Ring.type.
+check_join CountRing.Ring.type Equality.type CountRing.Ring.type.
+check_join CountRing.Ring.type FinGroup.type FinRing.Ring.type.
+check_join CountRing.Ring.type FinRing.Algebra.type FinRing.Algebra.type.
+check_join CountRing.Ring.type FinRing.ComRing.type FinRing.ComRing.type.
+check_join CountRing.Ring.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join CountRing.Ring.type FinRing.Field.type FinRing.Field.type.
+check_join CountRing.Ring.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join CountRing.Ring.type FinRing.Lalgebra.type FinRing.Lalgebra.type.
+check_join CountRing.Ring.type FinRing.Lmodule.type FinRing.Lalgebra.type.
+check_join CountRing.Ring.type FinRing.Ring.type FinRing.Ring.type.
+check_join CountRing.Ring.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join CountRing.Ring.type FinRing.UnitRing.type FinRing.UnitRing.type.
+check_join CountRing.Ring.type FinRing.Zmodule.type FinRing.Ring.type.
+check_join CountRing.Ring.type Finite.type FinRing.Ring.type.
+check_join CountRing.Ring.type GRing.Algebra.type FinRing.Algebra.type.
+check_join CountRing.Ring.type GRing.ClosedField.type CountRing.ClosedField.type.
+check_join CountRing.Ring.type GRing.ComRing.type CountRing.ComRing.type.
+check_join CountRing.Ring.type GRing.ComUnitRing.type CountRing.ComUnitRing.type.
+check_join CountRing.Ring.type GRing.DecidableField.type CountRing.DecidableField.type.
+check_join CountRing.Ring.type GRing.Field.type CountRing.Field.type.
+check_join CountRing.Ring.type GRing.IntegralDomain.type CountRing.IntegralDomain.type.
+check_join CountRing.Ring.type GRing.Lalgebra.type FinRing.Lalgebra.type.
+check_join CountRing.Ring.type GRing.Lmodule.type FinRing.Lalgebra.type.
+check_join CountRing.Ring.type GRing.Ring.type CountRing.Ring.type.
+check_join CountRing.Ring.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join CountRing.Ring.type GRing.UnitRing.type CountRing.UnitRing.type.
+check_join CountRing.Ring.type GRing.Zmodule.type CountRing.Ring.type.
+check_join CountRing.UnitRing.type Choice.type CountRing.UnitRing.type.
+check_join CountRing.UnitRing.type CountRing.ClosedField.type CountRing.ClosedField.type.
+check_join CountRing.UnitRing.type CountRing.ComRing.type CountRing.ComUnitRing.type.
+check_join CountRing.UnitRing.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type.
+check_join CountRing.UnitRing.type CountRing.DecidableField.type CountRing.DecidableField.type.
+check_join CountRing.UnitRing.type CountRing.Field.type CountRing.Field.type.
+check_join CountRing.UnitRing.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type.
+check_join CountRing.UnitRing.type CountRing.Ring.type CountRing.UnitRing.type.
+check_join CountRing.UnitRing.type CountRing.UnitRing.type CountRing.UnitRing.type.
+check_join CountRing.UnitRing.type CountRing.Zmodule.type CountRing.UnitRing.type.
+check_join CountRing.UnitRing.type Countable.type CountRing.UnitRing.type.
+check_join CountRing.UnitRing.type Equality.type CountRing.UnitRing.type.
+check_join CountRing.UnitRing.type FinGroup.type FinRing.UnitRing.type.
+check_join CountRing.UnitRing.type FinRing.Algebra.type FinRing.UnitAlgebra.type.
+check_join CountRing.UnitRing.type FinRing.ComRing.type FinRing.ComUnitRing.type.
+check_join CountRing.UnitRing.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join CountRing.UnitRing.type FinRing.Field.type FinRing.Field.type.
+check_join CountRing.UnitRing.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join CountRing.UnitRing.type FinRing.Lalgebra.type FinRing.UnitAlgebra.type.
+check_join CountRing.UnitRing.type FinRing.Lmodule.type FinRing.UnitAlgebra.type.
+check_join CountRing.UnitRing.type FinRing.Ring.type FinRing.UnitRing.type.
+check_join CountRing.UnitRing.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join CountRing.UnitRing.type FinRing.UnitRing.type FinRing.UnitRing.type.
+check_join CountRing.UnitRing.type FinRing.Zmodule.type FinRing.UnitRing.type.
+check_join CountRing.UnitRing.type Finite.type FinRing.UnitRing.type.
+check_join CountRing.UnitRing.type GRing.Algebra.type FinRing.UnitAlgebra.type.
+check_join CountRing.UnitRing.type GRing.ClosedField.type CountRing.ClosedField.type.
+check_join CountRing.UnitRing.type GRing.ComRing.type CountRing.ComUnitRing.type.
+check_join CountRing.UnitRing.type GRing.ComUnitRing.type CountRing.ComUnitRing.type.
+check_join CountRing.UnitRing.type GRing.DecidableField.type CountRing.DecidableField.type.
+check_join CountRing.UnitRing.type GRing.Field.type CountRing.Field.type.
+check_join CountRing.UnitRing.type GRing.IntegralDomain.type CountRing.IntegralDomain.type.
+check_join CountRing.UnitRing.type GRing.Lalgebra.type FinRing.UnitAlgebra.type.
+check_join CountRing.UnitRing.type GRing.Lmodule.type FinRing.UnitAlgebra.type.
+check_join CountRing.UnitRing.type GRing.Ring.type CountRing.UnitRing.type.
+check_join CountRing.UnitRing.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join CountRing.UnitRing.type GRing.UnitRing.type CountRing.UnitRing.type.
+check_join CountRing.UnitRing.type GRing.Zmodule.type CountRing.UnitRing.type.
+check_join CountRing.Zmodule.type Choice.type CountRing.Zmodule.type.
+check_join CountRing.Zmodule.type CountRing.ClosedField.type CountRing.ClosedField.type.
+check_join CountRing.Zmodule.type CountRing.ComRing.type CountRing.ComRing.type.
+check_join CountRing.Zmodule.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type.
+check_join CountRing.Zmodule.type CountRing.DecidableField.type CountRing.DecidableField.type.
+check_join CountRing.Zmodule.type CountRing.Field.type CountRing.Field.type.
+check_join CountRing.Zmodule.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type.
+check_join CountRing.Zmodule.type CountRing.Ring.type CountRing.Ring.type.
+check_join CountRing.Zmodule.type CountRing.UnitRing.type CountRing.UnitRing.type.
+check_join CountRing.Zmodule.type CountRing.Zmodule.type CountRing.Zmodule.type.
+check_join CountRing.Zmodule.type Countable.type CountRing.Zmodule.type.
+check_join CountRing.Zmodule.type Equality.type CountRing.Zmodule.type.
+check_join CountRing.Zmodule.type FinGroup.type FinRing.Zmodule.type.
+check_join CountRing.Zmodule.type FinRing.Algebra.type FinRing.Algebra.type.
+check_join CountRing.Zmodule.type FinRing.ComRing.type FinRing.ComRing.type.
+check_join CountRing.Zmodule.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join CountRing.Zmodule.type FinRing.Field.type FinRing.Field.type.
+check_join CountRing.Zmodule.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join CountRing.Zmodule.type FinRing.Lalgebra.type FinRing.Lalgebra.type.
+check_join CountRing.Zmodule.type FinRing.Lmodule.type FinRing.Lmodule.type.
+check_join CountRing.Zmodule.type FinRing.Ring.type FinRing.Ring.type.
+check_join CountRing.Zmodule.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join CountRing.Zmodule.type FinRing.UnitRing.type FinRing.UnitRing.type.
+check_join CountRing.Zmodule.type FinRing.Zmodule.type FinRing.Zmodule.type.
+check_join CountRing.Zmodule.type Finite.type FinRing.Zmodule.type.
+check_join CountRing.Zmodule.type GRing.Algebra.type FinRing.Algebra.type.
+check_join CountRing.Zmodule.type GRing.ClosedField.type CountRing.ClosedField.type.
+check_join CountRing.Zmodule.type GRing.ComRing.type CountRing.ComRing.type.
+check_join CountRing.Zmodule.type GRing.ComUnitRing.type CountRing.ComUnitRing.type.
+check_join CountRing.Zmodule.type GRing.DecidableField.type CountRing.DecidableField.type.
+check_join CountRing.Zmodule.type GRing.Field.type CountRing.Field.type.
+check_join CountRing.Zmodule.type GRing.IntegralDomain.type CountRing.IntegralDomain.type.
+check_join CountRing.Zmodule.type GRing.Lalgebra.type FinRing.Lalgebra.type.
+check_join CountRing.Zmodule.type GRing.Lmodule.type FinRing.Lmodule.type.
+check_join CountRing.Zmodule.type GRing.Ring.type CountRing.Ring.type.
+check_join CountRing.Zmodule.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join CountRing.Zmodule.type GRing.UnitRing.type CountRing.UnitRing.type.
+check_join CountRing.Zmodule.type GRing.Zmodule.type CountRing.Zmodule.type.
+check_join Countable.type Choice.type Countable.type.
+check_join Countable.type CountRing.ClosedField.type CountRing.ClosedField.type.
+check_join Countable.type CountRing.ComRing.type CountRing.ComRing.type.
+check_join Countable.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type.
+check_join Countable.type CountRing.DecidableField.type CountRing.DecidableField.type.
+check_join Countable.type CountRing.Field.type CountRing.Field.type.
+check_join Countable.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type.
+check_join Countable.type CountRing.Ring.type CountRing.Ring.type.
+check_join Countable.type CountRing.UnitRing.type CountRing.UnitRing.type.
+check_join Countable.type CountRing.Zmodule.type CountRing.Zmodule.type.
+check_join Countable.type Countable.type Countable.type.
+check_join Countable.type Equality.type Countable.type.
+check_join Countable.type FinGroup.type FinGroup.type.
+check_join Countable.type FinRing.Algebra.type FinRing.Algebra.type.
+check_join Countable.type FinRing.ComRing.type FinRing.ComRing.type.
+check_join Countable.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join Countable.type FinRing.Field.type FinRing.Field.type.
+check_join Countable.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join Countable.type FinRing.Lalgebra.type FinRing.Lalgebra.type.
+check_join Countable.type FinRing.Lmodule.type FinRing.Lmodule.type.
+check_join Countable.type FinRing.Ring.type FinRing.Ring.type.
+check_join Countable.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join Countable.type FinRing.UnitRing.type FinRing.UnitRing.type.
+check_join Countable.type FinRing.Zmodule.type FinRing.Zmodule.type.
+check_join Countable.type Finite.type Finite.type.
+check_join Countable.type GRing.Algebra.type FinRing.Algebra.type.
+check_join Countable.type GRing.ClosedField.type CountRing.ClosedField.type.
+check_join Countable.type GRing.ComRing.type CountRing.ComRing.type.
+check_join Countable.type GRing.ComUnitRing.type CountRing.ComUnitRing.type.
+check_join Countable.type GRing.DecidableField.type CountRing.DecidableField.type.
+check_join Countable.type GRing.Field.type CountRing.Field.type.
+check_join Countable.type GRing.IntegralDomain.type CountRing.IntegralDomain.type.
+check_join Countable.type GRing.Lalgebra.type FinRing.Lalgebra.type.
+check_join Countable.type GRing.Lmodule.type FinRing.Lmodule.type.
+check_join Countable.type GRing.Ring.type CountRing.Ring.type.
+check_join Countable.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join Countable.type GRing.UnitRing.type CountRing.UnitRing.type.
+check_join Countable.type GRing.Zmodule.type CountRing.Zmodule.type.
+check_join Equality.type Choice.type Choice.type.
+check_join Equality.type CountRing.ClosedField.type CountRing.ClosedField.type.
+check_join Equality.type CountRing.ComRing.type CountRing.ComRing.type.
+check_join Equality.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type.
+check_join Equality.type CountRing.DecidableField.type CountRing.DecidableField.type.
+check_join Equality.type CountRing.Field.type CountRing.Field.type.
+check_join Equality.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type.
+check_join Equality.type CountRing.Ring.type CountRing.Ring.type.
+check_join Equality.type CountRing.UnitRing.type CountRing.UnitRing.type.
+check_join Equality.type CountRing.Zmodule.type CountRing.Zmodule.type.
+check_join Equality.type Countable.type Countable.type.
+check_join Equality.type Equality.type Equality.type.
+check_join Equality.type Falgebra.type Falgebra.type.
+check_join Equality.type FieldExt.type FieldExt.type.
+check_join Equality.type FinGroup.type FinGroup.type.
+check_join Equality.type FinRing.Algebra.type FinRing.Algebra.type.
+check_join Equality.type FinRing.ComRing.type FinRing.ComRing.type.
+check_join Equality.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join Equality.type FinRing.Field.type FinRing.Field.type.
+check_join Equality.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join Equality.type FinRing.Lalgebra.type FinRing.Lalgebra.type.
+check_join Equality.type FinRing.Lmodule.type FinRing.Lmodule.type.
+check_join Equality.type FinRing.Ring.type FinRing.Ring.type.
+check_join Equality.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join Equality.type FinRing.UnitRing.type FinRing.UnitRing.type.
+check_join Equality.type FinRing.Zmodule.type FinRing.Zmodule.type.
+check_join Equality.type Finite.type Finite.type.
+check_join Equality.type GRing.Algebra.type GRing.Algebra.type.
+check_join Equality.type GRing.ClosedField.type GRing.ClosedField.type.
+check_join Equality.type GRing.ComRing.type GRing.ComRing.type.
+check_join Equality.type GRing.ComUnitRing.type GRing.ComUnitRing.type.
+check_join Equality.type GRing.DecidableField.type GRing.DecidableField.type.
+check_join Equality.type GRing.Field.type GRing.Field.type.
+check_join Equality.type GRing.IntegralDomain.type GRing.IntegralDomain.type.
+check_join Equality.type GRing.Lalgebra.type GRing.Lalgebra.type.
+check_join Equality.type GRing.Lmodule.type GRing.Lmodule.type.
+check_join Equality.type GRing.Ring.type GRing.Ring.type.
+check_join Equality.type GRing.UnitAlgebra.type GRing.UnitAlgebra.type.
+check_join Equality.type GRing.UnitRing.type GRing.UnitRing.type.
+check_join Equality.type GRing.Zmodule.type GRing.Zmodule.type.
+check_join Equality.type Num.ArchimedeanField.type Num.ArchimedeanField.type.
+check_join Equality.type Num.ClosedField.type Num.ClosedField.type.
+check_join Equality.type Num.NumDomain.type Num.NumDomain.type.
+check_join Equality.type Num.NumField.type Num.NumField.type.
+check_join Equality.type Num.RealClosedField.type Num.RealClosedField.type.
+check_join Equality.type Num.RealDomain.type Num.RealDomain.type.
+check_join Equality.type Num.RealField.type Num.RealField.type.
+check_join Equality.type SplittingField.type SplittingField.type.
+check_join Equality.type Vector.type Vector.type.
+check_join Falgebra.type Choice.type Falgebra.type.
+check_join Falgebra.type Equality.type Falgebra.type.
+check_join Falgebra.type Falgebra.type Falgebra.type.
+check_join Falgebra.type FieldExt.type FieldExt.type.
+check_join Falgebra.type GRing.Algebra.type Falgebra.type.
+check_join Falgebra.type GRing.ComRing.type FieldExt.type.
+check_join Falgebra.type GRing.ComUnitRing.type FieldExt.type.
+check_join Falgebra.type GRing.Field.type FieldExt.type.
+check_join Falgebra.type GRing.IntegralDomain.type FieldExt.type.
+check_join Falgebra.type GRing.Lalgebra.type Falgebra.type.
+check_join Falgebra.type GRing.Lmodule.type Falgebra.type.
+check_join Falgebra.type GRing.Ring.type Falgebra.type.
+check_join Falgebra.type GRing.UnitAlgebra.type Falgebra.type.
+check_join Falgebra.type GRing.UnitRing.type Falgebra.type.
+check_join Falgebra.type GRing.Zmodule.type Falgebra.type.
+check_join Falgebra.type SplittingField.type SplittingField.type.
+check_join Falgebra.type Vector.type Falgebra.type.
+check_join FieldExt.type Choice.type FieldExt.type.
+check_join FieldExt.type Equality.type FieldExt.type.
+check_join FieldExt.type Falgebra.type FieldExt.type.
+check_join FieldExt.type FieldExt.type FieldExt.type.
+check_join FieldExt.type GRing.Algebra.type FieldExt.type.
+check_join FieldExt.type GRing.ComRing.type FieldExt.type.
+check_join FieldExt.type GRing.ComUnitRing.type FieldExt.type.
+check_join FieldExt.type GRing.Field.type FieldExt.type.
+check_join FieldExt.type GRing.IntegralDomain.type FieldExt.type.
+check_join FieldExt.type GRing.Lalgebra.type FieldExt.type.
+check_join FieldExt.type GRing.Lmodule.type FieldExt.type.
+check_join FieldExt.type GRing.Ring.type FieldExt.type.
+check_join FieldExt.type GRing.UnitAlgebra.type FieldExt.type.
+check_join FieldExt.type GRing.UnitRing.type FieldExt.type.
+check_join FieldExt.type GRing.Zmodule.type FieldExt.type.
+check_join FieldExt.type SplittingField.type SplittingField.type.
+check_join FieldExt.type Vector.type FieldExt.type.
+check_join FinGroup.type Choice.type FinGroup.type.
+check_join FinGroup.type CountRing.ComRing.type FinRing.ComRing.type.
+check_join FinGroup.type CountRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join FinGroup.type CountRing.Field.type FinRing.Field.type.
+check_join FinGroup.type CountRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join FinGroup.type CountRing.Ring.type FinRing.Ring.type.
+check_join FinGroup.type CountRing.UnitRing.type FinRing.UnitRing.type.
+check_join FinGroup.type CountRing.Zmodule.type FinRing.Zmodule.type.
+check_join FinGroup.type Countable.type FinGroup.type.
+check_join FinGroup.type Equality.type FinGroup.type.
+check_join FinGroup.type FinGroup.type FinGroup.type.
+check_join FinGroup.type FinRing.Algebra.type FinRing.Algebra.type.
+check_join FinGroup.type FinRing.ComRing.type FinRing.ComRing.type.
+check_join FinGroup.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join FinGroup.type FinRing.Field.type FinRing.Field.type.
+check_join FinGroup.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join FinGroup.type FinRing.Lalgebra.type FinRing.Lalgebra.type.
+check_join FinGroup.type FinRing.Lmodule.type FinRing.Lmodule.type.
+check_join FinGroup.type FinRing.Ring.type FinRing.Ring.type.
+check_join FinGroup.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join FinGroup.type FinRing.UnitRing.type FinRing.UnitRing.type.
+check_join FinGroup.type FinRing.Zmodule.type FinRing.Zmodule.type.
+check_join FinGroup.type Finite.type FinGroup.type.
+check_join FinGroup.type GRing.Algebra.type FinRing.Algebra.type.
+check_join FinGroup.type GRing.ComRing.type FinRing.ComRing.type.
+check_join FinGroup.type GRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join FinGroup.type GRing.Field.type FinRing.Field.type.
+check_join FinGroup.type GRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join FinGroup.type GRing.Lalgebra.type FinRing.Lalgebra.type.
+check_join FinGroup.type GRing.Lmodule.type FinRing.Lmodule.type.
+check_join FinGroup.type GRing.Ring.type FinRing.Ring.type.
+check_join FinGroup.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join FinGroup.type GRing.UnitRing.type FinRing.UnitRing.type.
+check_join FinGroup.type GRing.Zmodule.type FinRing.Zmodule.type.
+check_join FinRing.Algebra.type Choice.type FinRing.Algebra.type.
+check_join FinRing.Algebra.type CountRing.Ring.type FinRing.Algebra.type.
+check_join FinRing.Algebra.type CountRing.UnitRing.type FinRing.UnitAlgebra.type.
+check_join FinRing.Algebra.type CountRing.Zmodule.type FinRing.Algebra.type.
+check_join FinRing.Algebra.type Countable.type FinRing.Algebra.type.
+check_join FinRing.Algebra.type Equality.type FinRing.Algebra.type.
+check_join FinRing.Algebra.type FinGroup.type FinRing.Algebra.type.
+check_join FinRing.Algebra.type FinRing.Algebra.type FinRing.Algebra.type.
+check_join FinRing.Algebra.type FinRing.Lalgebra.type FinRing.Algebra.type.
+check_join FinRing.Algebra.type FinRing.Lmodule.type FinRing.Algebra.type.
+check_join FinRing.Algebra.type FinRing.Ring.type FinRing.Algebra.type.
+check_join FinRing.Algebra.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join FinRing.Algebra.type FinRing.UnitRing.type FinRing.UnitAlgebra.type.
+check_join FinRing.Algebra.type FinRing.Zmodule.type FinRing.Algebra.type.
+check_join FinRing.Algebra.type Finite.type FinRing.Algebra.type.
+check_join FinRing.Algebra.type GRing.Algebra.type FinRing.Algebra.type.
+check_join FinRing.Algebra.type GRing.Lalgebra.type FinRing.Algebra.type.
+check_join FinRing.Algebra.type GRing.Lmodule.type FinRing.Algebra.type.
+check_join FinRing.Algebra.type GRing.Ring.type FinRing.Algebra.type.
+check_join FinRing.Algebra.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join FinRing.Algebra.type GRing.UnitRing.type FinRing.UnitAlgebra.type.
+check_join FinRing.Algebra.type GRing.Zmodule.type FinRing.Algebra.type.
+check_join FinRing.ComRing.type Choice.type FinRing.ComRing.type.
+check_join FinRing.ComRing.type CountRing.ComRing.type FinRing.ComRing.type.
+check_join FinRing.ComRing.type CountRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join FinRing.ComRing.type CountRing.Field.type FinRing.Field.type.
+check_join FinRing.ComRing.type CountRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join FinRing.ComRing.type CountRing.Ring.type FinRing.ComRing.type.
+check_join FinRing.ComRing.type CountRing.UnitRing.type FinRing.ComUnitRing.type.
+check_join FinRing.ComRing.type CountRing.Zmodule.type FinRing.ComRing.type.
+check_join FinRing.ComRing.type Countable.type FinRing.ComRing.type.
+check_join FinRing.ComRing.type Equality.type FinRing.ComRing.type.
+check_join FinRing.ComRing.type FinGroup.type FinRing.ComRing.type.
+check_join FinRing.ComRing.type FinRing.ComRing.type FinRing.ComRing.type.
+check_join FinRing.ComRing.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join FinRing.ComRing.type FinRing.Field.type FinRing.Field.type.
+check_join FinRing.ComRing.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join FinRing.ComRing.type FinRing.Ring.type FinRing.ComRing.type.
+check_join FinRing.ComRing.type FinRing.UnitRing.type FinRing.ComUnitRing.type.
+check_join FinRing.ComRing.type FinRing.Zmodule.type FinRing.ComRing.type.
+check_join FinRing.ComRing.type Finite.type FinRing.ComRing.type.
+check_join FinRing.ComRing.type GRing.ComRing.type FinRing.ComRing.type.
+check_join FinRing.ComRing.type GRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join FinRing.ComRing.type GRing.Field.type FinRing.Field.type.
+check_join FinRing.ComRing.type GRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join FinRing.ComRing.type GRing.Ring.type FinRing.ComRing.type.
+check_join FinRing.ComRing.type GRing.UnitRing.type FinRing.ComUnitRing.type.
+check_join FinRing.ComRing.type GRing.Zmodule.type FinRing.ComRing.type.
+check_join FinRing.ComUnitRing.type Choice.type FinRing.ComUnitRing.type.
+check_join FinRing.ComUnitRing.type CountRing.ComRing.type FinRing.ComUnitRing.type.
+check_join FinRing.ComUnitRing.type CountRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join FinRing.ComUnitRing.type CountRing.Field.type FinRing.Field.type.
+check_join FinRing.ComUnitRing.type CountRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join FinRing.ComUnitRing.type CountRing.Ring.type FinRing.ComUnitRing.type.
+check_join FinRing.ComUnitRing.type CountRing.UnitRing.type FinRing.ComUnitRing.type.
+check_join FinRing.ComUnitRing.type CountRing.Zmodule.type FinRing.ComUnitRing.type.
+check_join FinRing.ComUnitRing.type Countable.type FinRing.ComUnitRing.type.
+check_join FinRing.ComUnitRing.type Equality.type FinRing.ComUnitRing.type.
+check_join FinRing.ComUnitRing.type FinGroup.type FinRing.ComUnitRing.type.
+check_join FinRing.ComUnitRing.type FinRing.ComRing.type FinRing.ComUnitRing.type.
+check_join FinRing.ComUnitRing.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join FinRing.ComUnitRing.type FinRing.Field.type FinRing.Field.type.
+check_join FinRing.ComUnitRing.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join FinRing.ComUnitRing.type FinRing.Ring.type FinRing.ComUnitRing.type.
+check_join FinRing.ComUnitRing.type FinRing.UnitRing.type FinRing.ComUnitRing.type.
+check_join FinRing.ComUnitRing.type FinRing.Zmodule.type FinRing.ComUnitRing.type.
+check_join FinRing.ComUnitRing.type Finite.type FinRing.ComUnitRing.type.
+check_join FinRing.ComUnitRing.type GRing.ComRing.type FinRing.ComUnitRing.type.
+check_join FinRing.ComUnitRing.type GRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join FinRing.ComUnitRing.type GRing.Field.type FinRing.Field.type.
+check_join FinRing.ComUnitRing.type GRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join FinRing.ComUnitRing.type GRing.Ring.type FinRing.ComUnitRing.type.
+check_join FinRing.ComUnitRing.type GRing.UnitRing.type FinRing.ComUnitRing.type.
+check_join FinRing.ComUnitRing.type GRing.Zmodule.type FinRing.ComUnitRing.type.
+check_join FinRing.Field.type Choice.type FinRing.Field.type.
+check_join FinRing.Field.type CountRing.ComRing.type FinRing.Field.type.
+check_join FinRing.Field.type CountRing.ComUnitRing.type FinRing.Field.type.
+check_join FinRing.Field.type CountRing.Field.type FinRing.Field.type.
+check_join FinRing.Field.type CountRing.IntegralDomain.type FinRing.Field.type.
+check_join FinRing.Field.type CountRing.Ring.type FinRing.Field.type.
+check_join FinRing.Field.type CountRing.UnitRing.type FinRing.Field.type.
+check_join FinRing.Field.type CountRing.Zmodule.type FinRing.Field.type.
+check_join FinRing.Field.type Countable.type FinRing.Field.type.
+check_join FinRing.Field.type Equality.type FinRing.Field.type.
+check_join FinRing.Field.type FinGroup.type FinRing.Field.type.
+check_join FinRing.Field.type FinRing.ComRing.type FinRing.Field.type.
+check_join FinRing.Field.type FinRing.ComUnitRing.type FinRing.Field.type.
+check_join FinRing.Field.type FinRing.Field.type FinRing.Field.type.
+check_join FinRing.Field.type FinRing.IntegralDomain.type FinRing.Field.type.
+check_join FinRing.Field.type FinRing.Ring.type FinRing.Field.type.
+check_join FinRing.Field.type FinRing.UnitRing.type FinRing.Field.type.
+check_join FinRing.Field.type FinRing.Zmodule.type FinRing.Field.type.
+check_join FinRing.Field.type Finite.type FinRing.Field.type.
+check_join FinRing.Field.type GRing.ComRing.type FinRing.Field.type.
+check_join FinRing.Field.type GRing.ComUnitRing.type FinRing.Field.type.
+check_join FinRing.Field.type GRing.Field.type FinRing.Field.type.
+check_join FinRing.Field.type GRing.IntegralDomain.type FinRing.Field.type.
+check_join FinRing.Field.type GRing.Ring.type FinRing.Field.type.
+check_join FinRing.Field.type GRing.UnitRing.type FinRing.Field.type.
+check_join FinRing.Field.type GRing.Zmodule.type FinRing.Field.type.
+check_join FinRing.IntegralDomain.type Choice.type FinRing.IntegralDomain.type.
+check_join FinRing.IntegralDomain.type CountRing.ComRing.type FinRing.IntegralDomain.type.
+check_join FinRing.IntegralDomain.type CountRing.ComUnitRing.type FinRing.IntegralDomain.type.
+check_join FinRing.IntegralDomain.type CountRing.Field.type FinRing.Field.type.
+check_join FinRing.IntegralDomain.type CountRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join FinRing.IntegralDomain.type CountRing.Ring.type FinRing.IntegralDomain.type.
+check_join FinRing.IntegralDomain.type CountRing.UnitRing.type FinRing.IntegralDomain.type.
+check_join FinRing.IntegralDomain.type CountRing.Zmodule.type FinRing.IntegralDomain.type.
+check_join FinRing.IntegralDomain.type Countable.type FinRing.IntegralDomain.type.
+check_join FinRing.IntegralDomain.type Equality.type FinRing.IntegralDomain.type.
+check_join FinRing.IntegralDomain.type FinGroup.type FinRing.IntegralDomain.type.
+check_join FinRing.IntegralDomain.type FinRing.ComRing.type FinRing.IntegralDomain.type.
+check_join FinRing.IntegralDomain.type FinRing.ComUnitRing.type FinRing.IntegralDomain.type.
+check_join FinRing.IntegralDomain.type FinRing.Field.type FinRing.Field.type.
+check_join FinRing.IntegralDomain.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join FinRing.IntegralDomain.type FinRing.Ring.type FinRing.IntegralDomain.type.
+check_join FinRing.IntegralDomain.type FinRing.UnitRing.type FinRing.IntegralDomain.type.
+check_join FinRing.IntegralDomain.type FinRing.Zmodule.type FinRing.IntegralDomain.type.
+check_join FinRing.IntegralDomain.type Finite.type FinRing.IntegralDomain.type.
+check_join FinRing.IntegralDomain.type GRing.ComRing.type FinRing.IntegralDomain.type.
+check_join FinRing.IntegralDomain.type GRing.ComUnitRing.type FinRing.IntegralDomain.type.
+check_join FinRing.IntegralDomain.type GRing.Field.type FinRing.Field.type.
+check_join FinRing.IntegralDomain.type GRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join FinRing.IntegralDomain.type GRing.Ring.type FinRing.IntegralDomain.type.
+check_join FinRing.IntegralDomain.type GRing.UnitRing.type FinRing.IntegralDomain.type.
+check_join FinRing.IntegralDomain.type GRing.Zmodule.type FinRing.IntegralDomain.type.
+check_join FinRing.Lalgebra.type Choice.type FinRing.Lalgebra.type.
+check_join FinRing.Lalgebra.type CountRing.Ring.type FinRing.Lalgebra.type.
+check_join FinRing.Lalgebra.type CountRing.UnitRing.type FinRing.UnitAlgebra.type.
+check_join FinRing.Lalgebra.type CountRing.Zmodule.type FinRing.Lalgebra.type.
+check_join FinRing.Lalgebra.type Countable.type FinRing.Lalgebra.type.
+check_join FinRing.Lalgebra.type Equality.type FinRing.Lalgebra.type.
+check_join FinRing.Lalgebra.type FinGroup.type FinRing.Lalgebra.type.
+check_join FinRing.Lalgebra.type FinRing.Algebra.type FinRing.Algebra.type.
+check_join FinRing.Lalgebra.type FinRing.Lalgebra.type FinRing.Lalgebra.type.
+check_join FinRing.Lalgebra.type FinRing.Lmodule.type FinRing.Lalgebra.type.
+check_join FinRing.Lalgebra.type FinRing.Ring.type FinRing.Lalgebra.type.
+check_join FinRing.Lalgebra.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join FinRing.Lalgebra.type FinRing.UnitRing.type FinRing.UnitAlgebra.type.
+check_join FinRing.Lalgebra.type FinRing.Zmodule.type FinRing.Lalgebra.type.
+check_join FinRing.Lalgebra.type Finite.type FinRing.Lalgebra.type.
+check_join FinRing.Lalgebra.type GRing.Algebra.type FinRing.Algebra.type.
+check_join FinRing.Lalgebra.type GRing.Lalgebra.type FinRing.Lalgebra.type.
+check_join FinRing.Lalgebra.type GRing.Lmodule.type FinRing.Lalgebra.type.
+check_join FinRing.Lalgebra.type GRing.Ring.type FinRing.Lalgebra.type.
+check_join FinRing.Lalgebra.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join FinRing.Lalgebra.type GRing.UnitRing.type FinRing.UnitAlgebra.type.
+check_join FinRing.Lalgebra.type GRing.Zmodule.type FinRing.Lalgebra.type.
+check_join FinRing.Lmodule.type Choice.type FinRing.Lmodule.type.
+check_join FinRing.Lmodule.type CountRing.Ring.type FinRing.Lalgebra.type.
+check_join FinRing.Lmodule.type CountRing.UnitRing.type FinRing.UnitAlgebra.type.
+check_join FinRing.Lmodule.type CountRing.Zmodule.type FinRing.Lmodule.type.
+check_join FinRing.Lmodule.type Countable.type FinRing.Lmodule.type.
+check_join FinRing.Lmodule.type Equality.type FinRing.Lmodule.type.
+check_join FinRing.Lmodule.type FinGroup.type FinRing.Lmodule.type.
+check_join FinRing.Lmodule.type FinRing.Algebra.type FinRing.Algebra.type.
+check_join FinRing.Lmodule.type FinRing.Lalgebra.type FinRing.Lalgebra.type.
+check_join FinRing.Lmodule.type FinRing.Lmodule.type FinRing.Lmodule.type.
+check_join FinRing.Lmodule.type FinRing.Ring.type FinRing.Lalgebra.type.
+check_join FinRing.Lmodule.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join FinRing.Lmodule.type FinRing.UnitRing.type FinRing.UnitAlgebra.type.
+check_join FinRing.Lmodule.type FinRing.Zmodule.type FinRing.Lmodule.type.
+check_join FinRing.Lmodule.type Finite.type FinRing.Lmodule.type.
+check_join FinRing.Lmodule.type GRing.Algebra.type FinRing.Algebra.type.
+check_join FinRing.Lmodule.type GRing.Lalgebra.type FinRing.Lalgebra.type.
+check_join FinRing.Lmodule.type GRing.Lmodule.type FinRing.Lmodule.type.
+check_join FinRing.Lmodule.type GRing.Ring.type FinRing.Lalgebra.type.
+check_join FinRing.Lmodule.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join FinRing.Lmodule.type GRing.UnitRing.type FinRing.UnitAlgebra.type.
+check_join FinRing.Lmodule.type GRing.Zmodule.type FinRing.Lmodule.type.
+check_join FinRing.Ring.type Choice.type FinRing.Ring.type.
+check_join FinRing.Ring.type CountRing.ComRing.type FinRing.ComRing.type.
+check_join FinRing.Ring.type CountRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join FinRing.Ring.type CountRing.Field.type FinRing.Field.type.
+check_join FinRing.Ring.type CountRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join FinRing.Ring.type CountRing.Ring.type FinRing.Ring.type.
+check_join FinRing.Ring.type CountRing.UnitRing.type FinRing.UnitRing.type.
+check_join FinRing.Ring.type CountRing.Zmodule.type FinRing.Ring.type.
+check_join FinRing.Ring.type Countable.type FinRing.Ring.type.
+check_join FinRing.Ring.type Equality.type FinRing.Ring.type.
+check_join FinRing.Ring.type FinGroup.type FinRing.Ring.type.
+check_join FinRing.Ring.type FinRing.Algebra.type FinRing.Algebra.type.
+check_join FinRing.Ring.type FinRing.ComRing.type FinRing.ComRing.type.
+check_join FinRing.Ring.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join FinRing.Ring.type FinRing.Field.type FinRing.Field.type.
+check_join FinRing.Ring.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join FinRing.Ring.type FinRing.Lalgebra.type FinRing.Lalgebra.type.
+check_join FinRing.Ring.type FinRing.Lmodule.type FinRing.Lalgebra.type.
+check_join FinRing.Ring.type FinRing.Ring.type FinRing.Ring.type.
+check_join FinRing.Ring.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join FinRing.Ring.type FinRing.UnitRing.type FinRing.UnitRing.type.
+check_join FinRing.Ring.type FinRing.Zmodule.type FinRing.Ring.type.
+check_join FinRing.Ring.type Finite.type FinRing.Ring.type.
+check_join FinRing.Ring.type GRing.Algebra.type FinRing.Algebra.type.
+check_join FinRing.Ring.type GRing.ComRing.type FinRing.ComRing.type.
+check_join FinRing.Ring.type GRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join FinRing.Ring.type GRing.Field.type FinRing.Field.type.
+check_join FinRing.Ring.type GRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join FinRing.Ring.type GRing.Lalgebra.type FinRing.Lalgebra.type.
+check_join FinRing.Ring.type GRing.Lmodule.type FinRing.Lalgebra.type.
+check_join FinRing.Ring.type GRing.Ring.type FinRing.Ring.type.
+check_join FinRing.Ring.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join FinRing.Ring.type GRing.UnitRing.type FinRing.UnitRing.type.
+check_join FinRing.Ring.type GRing.Zmodule.type FinRing.Ring.type.
+check_join FinRing.UnitAlgebra.type Choice.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitAlgebra.type CountRing.Ring.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitAlgebra.type CountRing.UnitRing.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitAlgebra.type CountRing.Zmodule.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitAlgebra.type Countable.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitAlgebra.type Equality.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitAlgebra.type FinGroup.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitAlgebra.type FinRing.Algebra.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitAlgebra.type FinRing.Lalgebra.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitAlgebra.type FinRing.Lmodule.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitAlgebra.type FinRing.Ring.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitAlgebra.type FinRing.UnitRing.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitAlgebra.type FinRing.Zmodule.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitAlgebra.type Finite.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitAlgebra.type GRing.Algebra.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitAlgebra.type GRing.Lalgebra.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitAlgebra.type GRing.Lmodule.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitAlgebra.type GRing.Ring.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitAlgebra.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitAlgebra.type GRing.UnitRing.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitAlgebra.type GRing.Zmodule.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitRing.type Choice.type FinRing.UnitRing.type.
+check_join FinRing.UnitRing.type CountRing.ComRing.type FinRing.ComUnitRing.type.
+check_join FinRing.UnitRing.type CountRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join FinRing.UnitRing.type CountRing.Field.type FinRing.Field.type.
+check_join FinRing.UnitRing.type CountRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join FinRing.UnitRing.type CountRing.Ring.type FinRing.UnitRing.type.
+check_join FinRing.UnitRing.type CountRing.UnitRing.type FinRing.UnitRing.type.
+check_join FinRing.UnitRing.type CountRing.Zmodule.type FinRing.UnitRing.type.
+check_join FinRing.UnitRing.type Countable.type FinRing.UnitRing.type.
+check_join FinRing.UnitRing.type Equality.type FinRing.UnitRing.type.
+check_join FinRing.UnitRing.type FinGroup.type FinRing.UnitRing.type.
+check_join FinRing.UnitRing.type FinRing.Algebra.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitRing.type FinRing.ComRing.type FinRing.ComUnitRing.type.
+check_join FinRing.UnitRing.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join FinRing.UnitRing.type FinRing.Field.type FinRing.Field.type.
+check_join FinRing.UnitRing.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join FinRing.UnitRing.type FinRing.Lalgebra.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitRing.type FinRing.Lmodule.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitRing.type FinRing.Ring.type FinRing.UnitRing.type.
+check_join FinRing.UnitRing.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitRing.type FinRing.UnitRing.type FinRing.UnitRing.type.
+check_join FinRing.UnitRing.type FinRing.Zmodule.type FinRing.UnitRing.type.
+check_join FinRing.UnitRing.type Finite.type FinRing.UnitRing.type.
+check_join FinRing.UnitRing.type GRing.Algebra.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitRing.type GRing.ComRing.type FinRing.ComUnitRing.type.
+check_join FinRing.UnitRing.type GRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join FinRing.UnitRing.type GRing.Field.type FinRing.Field.type.
+check_join FinRing.UnitRing.type GRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join FinRing.UnitRing.type GRing.Lalgebra.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitRing.type GRing.Lmodule.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitRing.type GRing.Ring.type FinRing.UnitRing.type.
+check_join FinRing.UnitRing.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join FinRing.UnitRing.type GRing.UnitRing.type FinRing.UnitRing.type.
+check_join FinRing.UnitRing.type GRing.Zmodule.type FinRing.UnitRing.type.
+check_join FinRing.Zmodule.type Choice.type FinRing.Zmodule.type.
+check_join FinRing.Zmodule.type CountRing.ComRing.type FinRing.ComRing.type.
+check_join FinRing.Zmodule.type CountRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join FinRing.Zmodule.type CountRing.Field.type FinRing.Field.type.
+check_join FinRing.Zmodule.type CountRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join FinRing.Zmodule.type CountRing.Ring.type FinRing.Ring.type.
+check_join FinRing.Zmodule.type CountRing.UnitRing.type FinRing.UnitRing.type.
+check_join FinRing.Zmodule.type CountRing.Zmodule.type FinRing.Zmodule.type.
+check_join FinRing.Zmodule.type Countable.type FinRing.Zmodule.type.
+check_join FinRing.Zmodule.type Equality.type FinRing.Zmodule.type.
+check_join FinRing.Zmodule.type FinGroup.type FinRing.Zmodule.type.
+check_join FinRing.Zmodule.type FinRing.Algebra.type FinRing.Algebra.type.
+check_join FinRing.Zmodule.type FinRing.ComRing.type FinRing.ComRing.type.
+check_join FinRing.Zmodule.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join FinRing.Zmodule.type FinRing.Field.type FinRing.Field.type.
+check_join FinRing.Zmodule.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join FinRing.Zmodule.type FinRing.Lalgebra.type FinRing.Lalgebra.type.
+check_join FinRing.Zmodule.type FinRing.Lmodule.type FinRing.Lmodule.type.
+check_join FinRing.Zmodule.type FinRing.Ring.type FinRing.Ring.type.
+check_join FinRing.Zmodule.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join FinRing.Zmodule.type FinRing.UnitRing.type FinRing.UnitRing.type.
+check_join FinRing.Zmodule.type FinRing.Zmodule.type FinRing.Zmodule.type.
+check_join FinRing.Zmodule.type Finite.type FinRing.Zmodule.type.
+check_join FinRing.Zmodule.type GRing.Algebra.type FinRing.Algebra.type.
+check_join FinRing.Zmodule.type GRing.ComRing.type FinRing.ComRing.type.
+check_join FinRing.Zmodule.type GRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join FinRing.Zmodule.type GRing.Field.type FinRing.Field.type.
+check_join FinRing.Zmodule.type GRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join FinRing.Zmodule.type GRing.Lalgebra.type FinRing.Lalgebra.type.
+check_join FinRing.Zmodule.type GRing.Lmodule.type FinRing.Lmodule.type.
+check_join FinRing.Zmodule.type GRing.Ring.type FinRing.Ring.type.
+check_join FinRing.Zmodule.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join FinRing.Zmodule.type GRing.UnitRing.type FinRing.UnitRing.type.
+check_join FinRing.Zmodule.type GRing.Zmodule.type FinRing.Zmodule.type.
+check_join Finite.type Choice.type Finite.type.
+check_join Finite.type CountRing.ComRing.type FinRing.ComRing.type.
+check_join Finite.type CountRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join Finite.type CountRing.Field.type FinRing.Field.type.
+check_join Finite.type CountRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join Finite.type CountRing.Ring.type FinRing.Ring.type.
+check_join Finite.type CountRing.UnitRing.type FinRing.UnitRing.type.
+check_join Finite.type CountRing.Zmodule.type FinRing.Zmodule.type.
+check_join Finite.type Countable.type Finite.type.
+check_join Finite.type Equality.type Finite.type.
+check_join Finite.type FinGroup.type FinGroup.type.
+check_join Finite.type FinRing.Algebra.type FinRing.Algebra.type.
+check_join Finite.type FinRing.ComRing.type FinRing.ComRing.type.
+check_join Finite.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join Finite.type FinRing.Field.type FinRing.Field.type.
+check_join Finite.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join Finite.type FinRing.Lalgebra.type FinRing.Lalgebra.type.
+check_join Finite.type FinRing.Lmodule.type FinRing.Lmodule.type.
+check_join Finite.type FinRing.Ring.type FinRing.Ring.type.
+check_join Finite.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join Finite.type FinRing.UnitRing.type FinRing.UnitRing.type.
+check_join Finite.type FinRing.Zmodule.type FinRing.Zmodule.type.
+check_join Finite.type Finite.type Finite.type.
+check_join Finite.type GRing.Algebra.type FinRing.Algebra.type.
+check_join Finite.type GRing.ComRing.type FinRing.ComRing.type.
+check_join Finite.type GRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join Finite.type GRing.Field.type FinRing.Field.type.
+check_join Finite.type GRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join Finite.type GRing.Lalgebra.type FinRing.Lalgebra.type.
+check_join Finite.type GRing.Lmodule.type FinRing.Lmodule.type.
+check_join Finite.type GRing.Ring.type FinRing.Ring.type.
+check_join Finite.type GRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join Finite.type GRing.UnitRing.type FinRing.UnitRing.type.
+check_join Finite.type GRing.Zmodule.type FinRing.Zmodule.type.
+check_join GRing.Algebra.type Choice.type GRing.Algebra.type.
+check_join GRing.Algebra.type CountRing.Ring.type FinRing.Algebra.type.
+check_join GRing.Algebra.type CountRing.UnitRing.type FinRing.UnitAlgebra.type.
+check_join GRing.Algebra.type CountRing.Zmodule.type FinRing.Algebra.type.
+check_join GRing.Algebra.type Countable.type FinRing.Algebra.type.
+check_join GRing.Algebra.type Equality.type GRing.Algebra.type.
+check_join GRing.Algebra.type Falgebra.type Falgebra.type.
+check_join GRing.Algebra.type FieldExt.type FieldExt.type.
+check_join GRing.Algebra.type FinGroup.type FinRing.Algebra.type.
+check_join GRing.Algebra.type FinRing.Algebra.type FinRing.Algebra.type.
+check_join GRing.Algebra.type FinRing.Lalgebra.type FinRing.Algebra.type.
+check_join GRing.Algebra.type FinRing.Lmodule.type FinRing.Algebra.type.
+check_join GRing.Algebra.type FinRing.Ring.type FinRing.Algebra.type.
+check_join GRing.Algebra.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join GRing.Algebra.type FinRing.UnitRing.type FinRing.UnitAlgebra.type.
+check_join GRing.Algebra.type FinRing.Zmodule.type FinRing.Algebra.type.
+check_join GRing.Algebra.type Finite.type FinRing.Algebra.type.
+check_join GRing.Algebra.type GRing.Algebra.type GRing.Algebra.type.
+check_join GRing.Algebra.type GRing.ComRing.type FieldExt.type.
+check_join GRing.Algebra.type GRing.ComUnitRing.type FieldExt.type.
+check_join GRing.Algebra.type GRing.Field.type FieldExt.type.
+check_join GRing.Algebra.type GRing.IntegralDomain.type FieldExt.type.
+check_join GRing.Algebra.type GRing.Lalgebra.type GRing.Algebra.type.
+check_join GRing.Algebra.type GRing.Lmodule.type GRing.Algebra.type.
+check_join GRing.Algebra.type GRing.Ring.type GRing.Algebra.type.
+check_join GRing.Algebra.type GRing.UnitAlgebra.type GRing.UnitAlgebra.type.
+check_join GRing.Algebra.type GRing.UnitRing.type GRing.UnitAlgebra.type.
+check_join GRing.Algebra.type GRing.Zmodule.type GRing.Algebra.type.
+check_join GRing.Algebra.type SplittingField.type SplittingField.type.
+check_join GRing.Algebra.type Vector.type Falgebra.type.
+check_join GRing.ClosedField.type Choice.type GRing.ClosedField.type.
+check_join GRing.ClosedField.type CountRing.ClosedField.type CountRing.ClosedField.type.
+check_join GRing.ClosedField.type CountRing.ComRing.type CountRing.ClosedField.type.
+check_join GRing.ClosedField.type CountRing.ComUnitRing.type CountRing.ClosedField.type.
+check_join GRing.ClosedField.type CountRing.DecidableField.type CountRing.ClosedField.type.
+check_join GRing.ClosedField.type CountRing.Field.type CountRing.ClosedField.type.
+check_join GRing.ClosedField.type CountRing.IntegralDomain.type CountRing.ClosedField.type.
+check_join GRing.ClosedField.type CountRing.Ring.type CountRing.ClosedField.type.
+check_join GRing.ClosedField.type CountRing.UnitRing.type CountRing.ClosedField.type.
+check_join GRing.ClosedField.type CountRing.Zmodule.type CountRing.ClosedField.type.
+check_join GRing.ClosedField.type Countable.type CountRing.ClosedField.type.
+check_join GRing.ClosedField.type Equality.type GRing.ClosedField.type.
+check_join GRing.ClosedField.type GRing.ClosedField.type GRing.ClosedField.type.
+check_join GRing.ClosedField.type GRing.ComRing.type GRing.ClosedField.type.
+check_join GRing.ClosedField.type GRing.ComUnitRing.type GRing.ClosedField.type.
+check_join GRing.ClosedField.type GRing.DecidableField.type GRing.ClosedField.type.
+check_join GRing.ClosedField.type GRing.Field.type GRing.ClosedField.type.
+check_join GRing.ClosedField.type GRing.IntegralDomain.type GRing.ClosedField.type.
+check_join GRing.ClosedField.type GRing.Ring.type GRing.ClosedField.type.
+check_join GRing.ClosedField.type GRing.UnitRing.type GRing.ClosedField.type.
+check_join GRing.ClosedField.type GRing.Zmodule.type GRing.ClosedField.type.
+check_join GRing.ClosedField.type Num.ClosedField.type Num.ClosedField.type.
+check_join GRing.ClosedField.type Num.NumDomain.type Num.ClosedField.type.
+check_join GRing.ClosedField.type Num.NumField.type Num.ClosedField.type.
+check_join GRing.ComRing.type Choice.type GRing.ComRing.type.
+check_join GRing.ComRing.type CountRing.ClosedField.type CountRing.ClosedField.type.
+check_join GRing.ComRing.type CountRing.ComRing.type CountRing.ComRing.type.
+check_join GRing.ComRing.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type.
+check_join GRing.ComRing.type CountRing.DecidableField.type CountRing.DecidableField.type.
+check_join GRing.ComRing.type CountRing.Field.type CountRing.Field.type.
+check_join GRing.ComRing.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type.
+check_join GRing.ComRing.type CountRing.Ring.type CountRing.ComRing.type.
+check_join GRing.ComRing.type CountRing.UnitRing.type CountRing.ComUnitRing.type.
+check_join GRing.ComRing.type CountRing.Zmodule.type CountRing.ComRing.type.
+check_join GRing.ComRing.type Countable.type CountRing.ComRing.type.
+check_join GRing.ComRing.type Equality.type GRing.ComRing.type.
+check_join GRing.ComRing.type Falgebra.type FieldExt.type.
+check_join GRing.ComRing.type FieldExt.type FieldExt.type.
+check_join GRing.ComRing.type FinGroup.type FinRing.ComRing.type.
+check_join GRing.ComRing.type FinRing.ComRing.type FinRing.ComRing.type.
+check_join GRing.ComRing.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join GRing.ComRing.type FinRing.Field.type FinRing.Field.type.
+check_join GRing.ComRing.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join GRing.ComRing.type FinRing.Ring.type FinRing.ComRing.type.
+check_join GRing.ComRing.type FinRing.UnitRing.type FinRing.ComUnitRing.type.
+check_join GRing.ComRing.type FinRing.Zmodule.type FinRing.ComRing.type.
+check_join GRing.ComRing.type Finite.type FinRing.ComRing.type.
+check_join GRing.ComRing.type GRing.Algebra.type FieldExt.type.
+check_join GRing.ComRing.type GRing.ClosedField.type GRing.ClosedField.type.
+check_join GRing.ComRing.type GRing.ComRing.type GRing.ComRing.type.
+check_join GRing.ComRing.type GRing.ComUnitRing.type GRing.ComUnitRing.type.
+check_join GRing.ComRing.type GRing.DecidableField.type GRing.DecidableField.type.
+check_join GRing.ComRing.type GRing.Field.type GRing.Field.type.
+check_join GRing.ComRing.type GRing.IntegralDomain.type GRing.IntegralDomain.type.
+check_join GRing.ComRing.type GRing.Lalgebra.type FieldExt.type.
+check_join GRing.ComRing.type GRing.Lmodule.type FieldExt.type.
+check_join GRing.ComRing.type GRing.Ring.type GRing.ComRing.type.
+check_join GRing.ComRing.type GRing.UnitAlgebra.type FieldExt.type.
+check_join GRing.ComRing.type GRing.UnitRing.type GRing.ComUnitRing.type.
+check_join GRing.ComRing.type GRing.Zmodule.type GRing.ComRing.type.
+check_join GRing.ComRing.type Num.ArchimedeanField.type Num.ArchimedeanField.type.
+check_join GRing.ComRing.type Num.ClosedField.type Num.ClosedField.type.
+check_join GRing.ComRing.type Num.NumDomain.type Num.NumDomain.type.
+check_join GRing.ComRing.type Num.NumField.type Num.NumField.type.
+check_join GRing.ComRing.type Num.RealClosedField.type Num.RealClosedField.type.
+check_join GRing.ComRing.type Num.RealDomain.type Num.RealDomain.type.
+check_join GRing.ComRing.type Num.RealField.type Num.RealField.type.
+check_join GRing.ComRing.type SplittingField.type SplittingField.type.
+check_join GRing.ComRing.type Vector.type FieldExt.type.
+check_join GRing.ComUnitRing.type Choice.type GRing.ComUnitRing.type.
+check_join GRing.ComUnitRing.type CountRing.ClosedField.type CountRing.ClosedField.type.
+check_join GRing.ComUnitRing.type CountRing.ComRing.type CountRing.ComUnitRing.type.
+check_join GRing.ComUnitRing.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type.
+check_join GRing.ComUnitRing.type CountRing.DecidableField.type CountRing.DecidableField.type.
+check_join GRing.ComUnitRing.type CountRing.Field.type CountRing.Field.type.
+check_join GRing.ComUnitRing.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type.
+check_join GRing.ComUnitRing.type CountRing.Ring.type CountRing.ComUnitRing.type.
+check_join GRing.ComUnitRing.type CountRing.UnitRing.type CountRing.ComUnitRing.type.
+check_join GRing.ComUnitRing.type CountRing.Zmodule.type CountRing.ComUnitRing.type.
+check_join GRing.ComUnitRing.type Countable.type CountRing.ComUnitRing.type.
+check_join GRing.ComUnitRing.type Equality.type GRing.ComUnitRing.type.
+check_join GRing.ComUnitRing.type Falgebra.type FieldExt.type.
+check_join GRing.ComUnitRing.type FieldExt.type FieldExt.type.
+check_join GRing.ComUnitRing.type FinGroup.type FinRing.ComUnitRing.type.
+check_join GRing.ComUnitRing.type FinRing.ComRing.type FinRing.ComUnitRing.type.
+check_join GRing.ComUnitRing.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join GRing.ComUnitRing.type FinRing.Field.type FinRing.Field.type.
+check_join GRing.ComUnitRing.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join GRing.ComUnitRing.type FinRing.Ring.type FinRing.ComUnitRing.type.
+check_join GRing.ComUnitRing.type FinRing.UnitRing.type FinRing.ComUnitRing.type.
+check_join GRing.ComUnitRing.type FinRing.Zmodule.type FinRing.ComUnitRing.type.
+check_join GRing.ComUnitRing.type Finite.type FinRing.ComUnitRing.type.
+check_join GRing.ComUnitRing.type GRing.Algebra.type FieldExt.type.
+check_join GRing.ComUnitRing.type GRing.ClosedField.type GRing.ClosedField.type.
+check_join GRing.ComUnitRing.type GRing.ComRing.type GRing.ComUnitRing.type.
+check_join GRing.ComUnitRing.type GRing.ComUnitRing.type GRing.ComUnitRing.type.
+check_join GRing.ComUnitRing.type GRing.DecidableField.type GRing.DecidableField.type.
+check_join GRing.ComUnitRing.type GRing.Field.type GRing.Field.type.
+check_join GRing.ComUnitRing.type GRing.IntegralDomain.type GRing.IntegralDomain.type.
+check_join GRing.ComUnitRing.type GRing.Lalgebra.type FieldExt.type.
+check_join GRing.ComUnitRing.type GRing.Lmodule.type FieldExt.type.
+check_join GRing.ComUnitRing.type GRing.Ring.type GRing.ComUnitRing.type.
+check_join GRing.ComUnitRing.type GRing.UnitAlgebra.type FieldExt.type.
+check_join GRing.ComUnitRing.type GRing.UnitRing.type GRing.ComUnitRing.type.
+check_join GRing.ComUnitRing.type GRing.Zmodule.type GRing.ComUnitRing.type.
+check_join GRing.ComUnitRing.type Num.ArchimedeanField.type Num.ArchimedeanField.type.
+check_join GRing.ComUnitRing.type Num.ClosedField.type Num.ClosedField.type.
+check_join GRing.ComUnitRing.type Num.NumDomain.type Num.NumDomain.type.
+check_join GRing.ComUnitRing.type Num.NumField.type Num.NumField.type.
+check_join GRing.ComUnitRing.type Num.RealClosedField.type Num.RealClosedField.type.
+check_join GRing.ComUnitRing.type Num.RealDomain.type Num.RealDomain.type.
+check_join GRing.ComUnitRing.type Num.RealField.type Num.RealField.type.
+check_join GRing.ComUnitRing.type SplittingField.type SplittingField.type.
+check_join GRing.ComUnitRing.type Vector.type FieldExt.type.
+check_join GRing.DecidableField.type Choice.type GRing.DecidableField.type.
+check_join GRing.DecidableField.type CountRing.ClosedField.type CountRing.ClosedField.type.
+check_join GRing.DecidableField.type CountRing.ComRing.type CountRing.DecidableField.type.
+check_join GRing.DecidableField.type CountRing.ComUnitRing.type CountRing.DecidableField.type.
+check_join GRing.DecidableField.type CountRing.DecidableField.type CountRing.DecidableField.type.
+check_join GRing.DecidableField.type CountRing.Field.type CountRing.DecidableField.type.
+check_join GRing.DecidableField.type CountRing.IntegralDomain.type CountRing.DecidableField.type.
+check_join GRing.DecidableField.type CountRing.Ring.type CountRing.DecidableField.type.
+check_join GRing.DecidableField.type CountRing.UnitRing.type CountRing.DecidableField.type.
+check_join GRing.DecidableField.type CountRing.Zmodule.type CountRing.DecidableField.type.
+check_join GRing.DecidableField.type Countable.type CountRing.DecidableField.type.
+check_join GRing.DecidableField.type Equality.type GRing.DecidableField.type.
+check_join GRing.DecidableField.type GRing.ClosedField.type GRing.ClosedField.type.
+check_join GRing.DecidableField.type GRing.ComRing.type GRing.DecidableField.type.
+check_join GRing.DecidableField.type GRing.ComUnitRing.type GRing.DecidableField.type.
+check_join GRing.DecidableField.type GRing.DecidableField.type GRing.DecidableField.type.
+check_join GRing.DecidableField.type GRing.Field.type GRing.DecidableField.type.
+check_join GRing.DecidableField.type GRing.IntegralDomain.type GRing.DecidableField.type.
+check_join GRing.DecidableField.type GRing.Ring.type GRing.DecidableField.type.
+check_join GRing.DecidableField.type GRing.UnitRing.type GRing.DecidableField.type.
+check_join GRing.DecidableField.type GRing.Zmodule.type GRing.DecidableField.type.
+check_join GRing.DecidableField.type Num.ClosedField.type Num.ClosedField.type.
+check_join GRing.DecidableField.type Num.NumDomain.type Num.ClosedField.type.
+check_join GRing.DecidableField.type Num.NumField.type Num.ClosedField.type.
+check_join GRing.Field.type Choice.type GRing.Field.type.
+check_join GRing.Field.type CountRing.ClosedField.type CountRing.ClosedField.type.
+check_join GRing.Field.type CountRing.ComRing.type CountRing.Field.type.
+check_join GRing.Field.type CountRing.ComUnitRing.type CountRing.Field.type.
+check_join GRing.Field.type CountRing.DecidableField.type CountRing.DecidableField.type.
+check_join GRing.Field.type CountRing.Field.type CountRing.Field.type.
+check_join GRing.Field.type CountRing.IntegralDomain.type CountRing.Field.type.
+check_join GRing.Field.type CountRing.Ring.type CountRing.Field.type.
+check_join GRing.Field.type CountRing.UnitRing.type CountRing.Field.type.
+check_join GRing.Field.type CountRing.Zmodule.type CountRing.Field.type.
+check_join GRing.Field.type Countable.type CountRing.Field.type.
+check_join GRing.Field.type Equality.type GRing.Field.type.
+check_join GRing.Field.type Falgebra.type FieldExt.type.
+check_join GRing.Field.type FieldExt.type FieldExt.type.
+check_join GRing.Field.type FinGroup.type FinRing.Field.type.
+check_join GRing.Field.type FinRing.ComRing.type FinRing.Field.type.
+check_join GRing.Field.type FinRing.ComUnitRing.type FinRing.Field.type.
+check_join GRing.Field.type FinRing.Field.type FinRing.Field.type.
+check_join GRing.Field.type FinRing.IntegralDomain.type FinRing.Field.type.
+check_join GRing.Field.type FinRing.Ring.type FinRing.Field.type.
+check_join GRing.Field.type FinRing.UnitRing.type FinRing.Field.type.
+check_join GRing.Field.type FinRing.Zmodule.type FinRing.Field.type.
+check_join GRing.Field.type Finite.type FinRing.Field.type.
+check_join GRing.Field.type GRing.Algebra.type FieldExt.type.
+check_join GRing.Field.type GRing.ClosedField.type GRing.ClosedField.type.
+check_join GRing.Field.type GRing.ComRing.type GRing.Field.type.
+check_join GRing.Field.type GRing.ComUnitRing.type GRing.Field.type.
+check_join GRing.Field.type GRing.DecidableField.type GRing.DecidableField.type.
+check_join GRing.Field.type GRing.Field.type GRing.Field.type.
+check_join GRing.Field.type GRing.IntegralDomain.type GRing.Field.type.
+check_join GRing.Field.type GRing.Lalgebra.type FieldExt.type.
+check_join GRing.Field.type GRing.Lmodule.type FieldExt.type.
+check_join GRing.Field.type GRing.Ring.type GRing.Field.type.
+check_join GRing.Field.type GRing.UnitAlgebra.type FieldExt.type.
+check_join GRing.Field.type GRing.UnitRing.type GRing.Field.type.
+check_join GRing.Field.type GRing.Zmodule.type GRing.Field.type.
+check_join GRing.Field.type Num.ArchimedeanField.type Num.ArchimedeanField.type.
+check_join GRing.Field.type Num.ClosedField.type Num.ClosedField.type.
+check_join GRing.Field.type Num.NumDomain.type Num.NumField.type.
+check_join GRing.Field.type Num.NumField.type Num.NumField.type.
+check_join GRing.Field.type Num.RealClosedField.type Num.RealClosedField.type.
+check_join GRing.Field.type Num.RealDomain.type Num.RealField.type.
+check_join GRing.Field.type Num.RealField.type Num.RealField.type.
+check_join GRing.Field.type SplittingField.type SplittingField.type.
+check_join GRing.Field.type Vector.type FieldExt.type.
+check_join GRing.IntegralDomain.type Choice.type GRing.IntegralDomain.type.
+check_join GRing.IntegralDomain.type CountRing.ClosedField.type CountRing.ClosedField.type.
+check_join GRing.IntegralDomain.type CountRing.ComRing.type CountRing.IntegralDomain.type.
+check_join GRing.IntegralDomain.type CountRing.ComUnitRing.type CountRing.IntegralDomain.type.
+check_join GRing.IntegralDomain.type CountRing.DecidableField.type CountRing.DecidableField.type.
+check_join GRing.IntegralDomain.type CountRing.Field.type CountRing.Field.type.
+check_join GRing.IntegralDomain.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type.
+check_join GRing.IntegralDomain.type CountRing.Ring.type CountRing.IntegralDomain.type.
+check_join GRing.IntegralDomain.type CountRing.UnitRing.type CountRing.IntegralDomain.type.
+check_join GRing.IntegralDomain.type CountRing.Zmodule.type CountRing.IntegralDomain.type.
+check_join GRing.IntegralDomain.type Countable.type CountRing.IntegralDomain.type.
+check_join GRing.IntegralDomain.type Equality.type GRing.IntegralDomain.type.
+check_join GRing.IntegralDomain.type Falgebra.type FieldExt.type.
+check_join GRing.IntegralDomain.type FieldExt.type FieldExt.type.
+check_join GRing.IntegralDomain.type FinGroup.type FinRing.IntegralDomain.type.
+check_join GRing.IntegralDomain.type FinRing.ComRing.type FinRing.IntegralDomain.type.
+check_join GRing.IntegralDomain.type FinRing.ComUnitRing.type FinRing.IntegralDomain.type.
+check_join GRing.IntegralDomain.type FinRing.Field.type FinRing.Field.type.
+check_join GRing.IntegralDomain.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join GRing.IntegralDomain.type FinRing.Ring.type FinRing.IntegralDomain.type.
+check_join GRing.IntegralDomain.type FinRing.UnitRing.type FinRing.IntegralDomain.type.
+check_join GRing.IntegralDomain.type FinRing.Zmodule.type FinRing.IntegralDomain.type.
+check_join GRing.IntegralDomain.type Finite.type FinRing.IntegralDomain.type.
+check_join GRing.IntegralDomain.type GRing.Algebra.type FieldExt.type.
+check_join GRing.IntegralDomain.type GRing.ClosedField.type GRing.ClosedField.type.
+check_join GRing.IntegralDomain.type GRing.ComRing.type GRing.IntegralDomain.type.
+check_join GRing.IntegralDomain.type GRing.ComUnitRing.type GRing.IntegralDomain.type.
+check_join GRing.IntegralDomain.type GRing.DecidableField.type GRing.DecidableField.type.
+check_join GRing.IntegralDomain.type GRing.Field.type GRing.Field.type.
+check_join GRing.IntegralDomain.type GRing.IntegralDomain.type GRing.IntegralDomain.type.
+check_join GRing.IntegralDomain.type GRing.Lalgebra.type FieldExt.type.
+check_join GRing.IntegralDomain.type GRing.Lmodule.type FieldExt.type.
+check_join GRing.IntegralDomain.type GRing.Ring.type GRing.IntegralDomain.type.
+check_join GRing.IntegralDomain.type GRing.UnitAlgebra.type FieldExt.type.
+check_join GRing.IntegralDomain.type GRing.UnitRing.type GRing.IntegralDomain.type.
+check_join GRing.IntegralDomain.type GRing.Zmodule.type GRing.IntegralDomain.type.
+check_join GRing.IntegralDomain.type Num.ArchimedeanField.type Num.ArchimedeanField.type.
+check_join GRing.IntegralDomain.type Num.ClosedField.type Num.ClosedField.type.
+check_join GRing.IntegralDomain.type Num.NumDomain.type Num.NumDomain.type.
+check_join GRing.IntegralDomain.type Num.NumField.type Num.NumField.type.
+check_join GRing.IntegralDomain.type Num.RealClosedField.type Num.RealClosedField.type.
+check_join GRing.IntegralDomain.type Num.RealDomain.type Num.RealDomain.type.
+check_join GRing.IntegralDomain.type Num.RealField.type Num.RealField.type.
+check_join GRing.IntegralDomain.type SplittingField.type SplittingField.type.
+check_join GRing.IntegralDomain.type Vector.type FieldExt.type.
+check_join GRing.Lalgebra.type Choice.type GRing.Lalgebra.type.
+check_join GRing.Lalgebra.type CountRing.Ring.type FinRing.Lalgebra.type.
+check_join GRing.Lalgebra.type CountRing.UnitRing.type FinRing.UnitAlgebra.type.
+check_join GRing.Lalgebra.type CountRing.Zmodule.type FinRing.Lalgebra.type.
+check_join GRing.Lalgebra.type Countable.type FinRing.Lalgebra.type.
+check_join GRing.Lalgebra.type Equality.type GRing.Lalgebra.type.
+check_join GRing.Lalgebra.type Falgebra.type Falgebra.type.
+check_join GRing.Lalgebra.type FieldExt.type FieldExt.type.
+check_join GRing.Lalgebra.type FinGroup.type FinRing.Lalgebra.type.
+check_join GRing.Lalgebra.type FinRing.Algebra.type FinRing.Algebra.type.
+check_join GRing.Lalgebra.type FinRing.Lalgebra.type FinRing.Lalgebra.type.
+check_join GRing.Lalgebra.type FinRing.Lmodule.type FinRing.Lalgebra.type.
+check_join GRing.Lalgebra.type FinRing.Ring.type FinRing.Lalgebra.type.
+check_join GRing.Lalgebra.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join GRing.Lalgebra.type FinRing.UnitRing.type FinRing.UnitAlgebra.type.
+check_join GRing.Lalgebra.type FinRing.Zmodule.type FinRing.Lalgebra.type.
+check_join GRing.Lalgebra.type Finite.type FinRing.Lalgebra.type.
+check_join GRing.Lalgebra.type GRing.Algebra.type GRing.Algebra.type.
+check_join GRing.Lalgebra.type GRing.ComRing.type FieldExt.type.
+check_join GRing.Lalgebra.type GRing.ComUnitRing.type FieldExt.type.
+check_join GRing.Lalgebra.type GRing.Field.type FieldExt.type.
+check_join GRing.Lalgebra.type GRing.IntegralDomain.type FieldExt.type.
+check_join GRing.Lalgebra.type GRing.Lalgebra.type GRing.Lalgebra.type.
+check_join GRing.Lalgebra.type GRing.Lmodule.type GRing.Lalgebra.type.
+check_join GRing.Lalgebra.type GRing.Ring.type GRing.Lalgebra.type.
+check_join GRing.Lalgebra.type GRing.UnitAlgebra.type GRing.UnitAlgebra.type.
+check_join GRing.Lalgebra.type GRing.UnitRing.type GRing.UnitAlgebra.type.
+check_join GRing.Lalgebra.type GRing.Zmodule.type GRing.Lalgebra.type.
+check_join GRing.Lalgebra.type SplittingField.type SplittingField.type.
+check_join GRing.Lalgebra.type Vector.type Falgebra.type.
+check_join GRing.Lmodule.type Choice.type GRing.Lmodule.type.
+check_join GRing.Lmodule.type CountRing.Ring.type FinRing.Lalgebra.type.
+check_join GRing.Lmodule.type CountRing.UnitRing.type FinRing.UnitAlgebra.type.
+check_join GRing.Lmodule.type CountRing.Zmodule.type FinRing.Lmodule.type.
+check_join GRing.Lmodule.type Countable.type FinRing.Lmodule.type.
+check_join GRing.Lmodule.type Equality.type GRing.Lmodule.type.
+check_join GRing.Lmodule.type Falgebra.type Falgebra.type.
+check_join GRing.Lmodule.type FieldExt.type FieldExt.type.
+check_join GRing.Lmodule.type FinGroup.type FinRing.Lmodule.type.
+check_join GRing.Lmodule.type FinRing.Algebra.type FinRing.Algebra.type.
+check_join GRing.Lmodule.type FinRing.Lalgebra.type FinRing.Lalgebra.type.
+check_join GRing.Lmodule.type FinRing.Lmodule.type FinRing.Lmodule.type.
+check_join GRing.Lmodule.type FinRing.Ring.type FinRing.Lalgebra.type.
+check_join GRing.Lmodule.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join GRing.Lmodule.type FinRing.UnitRing.type FinRing.UnitAlgebra.type.
+check_join GRing.Lmodule.type FinRing.Zmodule.type FinRing.Lmodule.type.
+check_join GRing.Lmodule.type Finite.type FinRing.Lmodule.type.
+check_join GRing.Lmodule.type GRing.Algebra.type GRing.Algebra.type.
+check_join GRing.Lmodule.type GRing.ComRing.type FieldExt.type.
+check_join GRing.Lmodule.type GRing.ComUnitRing.type FieldExt.type.
+check_join GRing.Lmodule.type GRing.Field.type FieldExt.type.
+check_join GRing.Lmodule.type GRing.IntegralDomain.type FieldExt.type.
+check_join GRing.Lmodule.type GRing.Lalgebra.type GRing.Lalgebra.type.
+check_join GRing.Lmodule.type GRing.Lmodule.type GRing.Lmodule.type.
+check_join GRing.Lmodule.type GRing.Ring.type GRing.Lalgebra.type.
+check_join GRing.Lmodule.type GRing.UnitAlgebra.type GRing.UnitAlgebra.type.
+check_join GRing.Lmodule.type GRing.UnitRing.type GRing.UnitAlgebra.type.
+check_join GRing.Lmodule.type GRing.Zmodule.type GRing.Lmodule.type.
+check_join GRing.Lmodule.type SplittingField.type SplittingField.type.
+check_join GRing.Lmodule.type Vector.type Vector.type.
+check_join GRing.Ring.type Choice.type GRing.Ring.type.
+check_join GRing.Ring.type CountRing.ClosedField.type CountRing.ClosedField.type.
+check_join GRing.Ring.type CountRing.ComRing.type CountRing.ComRing.type.
+check_join GRing.Ring.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type.
+check_join GRing.Ring.type CountRing.DecidableField.type CountRing.DecidableField.type.
+check_join GRing.Ring.type CountRing.Field.type CountRing.Field.type.
+check_join GRing.Ring.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type.
+check_join GRing.Ring.type CountRing.Ring.type CountRing.Ring.type.
+check_join GRing.Ring.type CountRing.UnitRing.type CountRing.UnitRing.type.
+check_join GRing.Ring.type CountRing.Zmodule.type CountRing.Ring.type.
+check_join GRing.Ring.type Countable.type CountRing.Ring.type.
+check_join GRing.Ring.type Equality.type GRing.Ring.type.
+check_join GRing.Ring.type Falgebra.type Falgebra.type.
+check_join GRing.Ring.type FieldExt.type FieldExt.type.
+check_join GRing.Ring.type FinGroup.type FinRing.Ring.type.
+check_join GRing.Ring.type FinRing.Algebra.type FinRing.Algebra.type.
+check_join GRing.Ring.type FinRing.ComRing.type FinRing.ComRing.type.
+check_join GRing.Ring.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join GRing.Ring.type FinRing.Field.type FinRing.Field.type.
+check_join GRing.Ring.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join GRing.Ring.type FinRing.Lalgebra.type FinRing.Lalgebra.type.
+check_join GRing.Ring.type FinRing.Lmodule.type FinRing.Lalgebra.type.
+check_join GRing.Ring.type FinRing.Ring.type FinRing.Ring.type.
+check_join GRing.Ring.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join GRing.Ring.type FinRing.UnitRing.type FinRing.UnitRing.type.
+check_join GRing.Ring.type FinRing.Zmodule.type FinRing.Ring.type.
+check_join GRing.Ring.type Finite.type FinRing.Ring.type.
+check_join GRing.Ring.type GRing.Algebra.type GRing.Algebra.type.
+check_join GRing.Ring.type GRing.ClosedField.type GRing.ClosedField.type.
+check_join GRing.Ring.type GRing.ComRing.type GRing.ComRing.type.
+check_join GRing.Ring.type GRing.ComUnitRing.type GRing.ComUnitRing.type.
+check_join GRing.Ring.type GRing.DecidableField.type GRing.DecidableField.type.
+check_join GRing.Ring.type GRing.Field.type GRing.Field.type.
+check_join GRing.Ring.type GRing.IntegralDomain.type GRing.IntegralDomain.type.
+check_join GRing.Ring.type GRing.Lalgebra.type GRing.Lalgebra.type.
+check_join GRing.Ring.type GRing.Lmodule.type GRing.Lalgebra.type.
+check_join GRing.Ring.type GRing.Ring.type GRing.Ring.type.
+check_join GRing.Ring.type GRing.UnitAlgebra.type GRing.UnitAlgebra.type.
+check_join GRing.Ring.type GRing.UnitRing.type GRing.UnitRing.type.
+check_join GRing.Ring.type GRing.Zmodule.type GRing.Ring.type.
+check_join GRing.Ring.type Num.ArchimedeanField.type Num.ArchimedeanField.type.
+check_join GRing.Ring.type Num.ClosedField.type Num.ClosedField.type.
+check_join GRing.Ring.type Num.NumDomain.type Num.NumDomain.type.
+check_join GRing.Ring.type Num.NumField.type Num.NumField.type.
+check_join GRing.Ring.type Num.RealClosedField.type Num.RealClosedField.type.
+check_join GRing.Ring.type Num.RealDomain.type Num.RealDomain.type.
+check_join GRing.Ring.type Num.RealField.type Num.RealField.type.
+check_join GRing.Ring.type SplittingField.type SplittingField.type.
+check_join GRing.Ring.type Vector.type Falgebra.type.
+check_join GRing.UnitAlgebra.type Choice.type GRing.UnitAlgebra.type.
+check_join GRing.UnitAlgebra.type CountRing.Ring.type FinRing.UnitAlgebra.type.
+check_join GRing.UnitAlgebra.type CountRing.UnitRing.type FinRing.UnitAlgebra.type.
+check_join GRing.UnitAlgebra.type CountRing.Zmodule.type FinRing.UnitAlgebra.type.
+check_join GRing.UnitAlgebra.type Countable.type FinRing.UnitAlgebra.type.
+check_join GRing.UnitAlgebra.type Equality.type GRing.UnitAlgebra.type.
+check_join GRing.UnitAlgebra.type Falgebra.type Falgebra.type.
+check_join GRing.UnitAlgebra.type FieldExt.type FieldExt.type.
+check_join GRing.UnitAlgebra.type FinGroup.type FinRing.UnitAlgebra.type.
+check_join GRing.UnitAlgebra.type FinRing.Algebra.type FinRing.UnitAlgebra.type.
+check_join GRing.UnitAlgebra.type FinRing.Lalgebra.type FinRing.UnitAlgebra.type.
+check_join GRing.UnitAlgebra.type FinRing.Lmodule.type FinRing.UnitAlgebra.type.
+check_join GRing.UnitAlgebra.type FinRing.Ring.type FinRing.UnitAlgebra.type.
+check_join GRing.UnitAlgebra.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join GRing.UnitAlgebra.type FinRing.UnitRing.type FinRing.UnitAlgebra.type.
+check_join GRing.UnitAlgebra.type FinRing.Zmodule.type FinRing.UnitAlgebra.type.
+check_join GRing.UnitAlgebra.type Finite.type FinRing.UnitAlgebra.type.
+check_join GRing.UnitAlgebra.type GRing.Algebra.type GRing.UnitAlgebra.type.
+check_join GRing.UnitAlgebra.type GRing.ComRing.type FieldExt.type.
+check_join GRing.UnitAlgebra.type GRing.ComUnitRing.type FieldExt.type.
+check_join GRing.UnitAlgebra.type GRing.Field.type FieldExt.type.
+check_join GRing.UnitAlgebra.type GRing.IntegralDomain.type FieldExt.type.
+check_join GRing.UnitAlgebra.type GRing.Lalgebra.type GRing.UnitAlgebra.type.
+check_join GRing.UnitAlgebra.type GRing.Lmodule.type GRing.UnitAlgebra.type.
+check_join GRing.UnitAlgebra.type GRing.Ring.type GRing.UnitAlgebra.type.
+check_join GRing.UnitAlgebra.type GRing.UnitAlgebra.type GRing.UnitAlgebra.type.
+check_join GRing.UnitAlgebra.type GRing.UnitRing.type GRing.UnitAlgebra.type.
+check_join GRing.UnitAlgebra.type GRing.Zmodule.type GRing.UnitAlgebra.type.
+check_join GRing.UnitAlgebra.type SplittingField.type SplittingField.type.
+check_join GRing.UnitAlgebra.type Vector.type Falgebra.type.
+check_join GRing.UnitRing.type Choice.type GRing.UnitRing.type.
+check_join GRing.UnitRing.type CountRing.ClosedField.type CountRing.ClosedField.type.
+check_join GRing.UnitRing.type CountRing.ComRing.type CountRing.ComUnitRing.type.
+check_join GRing.UnitRing.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type.
+check_join GRing.UnitRing.type CountRing.DecidableField.type CountRing.DecidableField.type.
+check_join GRing.UnitRing.type CountRing.Field.type CountRing.Field.type.
+check_join GRing.UnitRing.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type.
+check_join GRing.UnitRing.type CountRing.Ring.type CountRing.UnitRing.type.
+check_join GRing.UnitRing.type CountRing.UnitRing.type CountRing.UnitRing.type.
+check_join GRing.UnitRing.type CountRing.Zmodule.type CountRing.UnitRing.type.
+check_join GRing.UnitRing.type Countable.type CountRing.UnitRing.type.
+check_join GRing.UnitRing.type Equality.type GRing.UnitRing.type.
+check_join GRing.UnitRing.type Falgebra.type Falgebra.type.
+check_join GRing.UnitRing.type FieldExt.type FieldExt.type.
+check_join GRing.UnitRing.type FinGroup.type FinRing.UnitRing.type.
+check_join GRing.UnitRing.type FinRing.Algebra.type FinRing.UnitAlgebra.type.
+check_join GRing.UnitRing.type FinRing.ComRing.type FinRing.ComUnitRing.type.
+check_join GRing.UnitRing.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join GRing.UnitRing.type FinRing.Field.type FinRing.Field.type.
+check_join GRing.UnitRing.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join GRing.UnitRing.type FinRing.Lalgebra.type FinRing.UnitAlgebra.type.
+check_join GRing.UnitRing.type FinRing.Lmodule.type FinRing.UnitAlgebra.type.
+check_join GRing.UnitRing.type FinRing.Ring.type FinRing.UnitRing.type.
+check_join GRing.UnitRing.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join GRing.UnitRing.type FinRing.UnitRing.type FinRing.UnitRing.type.
+check_join GRing.UnitRing.type FinRing.Zmodule.type FinRing.UnitRing.type.
+check_join GRing.UnitRing.type Finite.type FinRing.UnitRing.type.
+check_join GRing.UnitRing.type GRing.Algebra.type GRing.UnitAlgebra.type.
+check_join GRing.UnitRing.type GRing.ClosedField.type GRing.ClosedField.type.
+check_join GRing.UnitRing.type GRing.ComRing.type GRing.ComUnitRing.type.
+check_join GRing.UnitRing.type GRing.ComUnitRing.type GRing.ComUnitRing.type.
+check_join GRing.UnitRing.type GRing.DecidableField.type GRing.DecidableField.type.
+check_join GRing.UnitRing.type GRing.Field.type GRing.Field.type.
+check_join GRing.UnitRing.type GRing.IntegralDomain.type GRing.IntegralDomain.type.
+check_join GRing.UnitRing.type GRing.Lalgebra.type GRing.UnitAlgebra.type.
+check_join GRing.UnitRing.type GRing.Lmodule.type GRing.UnitAlgebra.type.
+check_join GRing.UnitRing.type GRing.Ring.type GRing.UnitRing.type.
+check_join GRing.UnitRing.type GRing.UnitAlgebra.type GRing.UnitAlgebra.type.
+check_join GRing.UnitRing.type GRing.UnitRing.type GRing.UnitRing.type.
+check_join GRing.UnitRing.type GRing.Zmodule.type GRing.UnitRing.type.
+check_join GRing.UnitRing.type Num.ArchimedeanField.type Num.ArchimedeanField.type.
+check_join GRing.UnitRing.type Num.ClosedField.type Num.ClosedField.type.
+check_join GRing.UnitRing.type Num.NumDomain.type Num.NumDomain.type.
+check_join GRing.UnitRing.type Num.NumField.type Num.NumField.type.
+check_join GRing.UnitRing.type Num.RealClosedField.type Num.RealClosedField.type.
+check_join GRing.UnitRing.type Num.RealDomain.type Num.RealDomain.type.
+check_join GRing.UnitRing.type Num.RealField.type Num.RealField.type.
+check_join GRing.UnitRing.type SplittingField.type SplittingField.type.
+check_join GRing.UnitRing.type Vector.type Falgebra.type.
+check_join GRing.Zmodule.type Choice.type GRing.Zmodule.type.
+check_join GRing.Zmodule.type CountRing.ClosedField.type CountRing.ClosedField.type.
+check_join GRing.Zmodule.type CountRing.ComRing.type CountRing.ComRing.type.
+check_join GRing.Zmodule.type CountRing.ComUnitRing.type CountRing.ComUnitRing.type.
+check_join GRing.Zmodule.type CountRing.DecidableField.type CountRing.DecidableField.type.
+check_join GRing.Zmodule.type CountRing.Field.type CountRing.Field.type.
+check_join GRing.Zmodule.type CountRing.IntegralDomain.type CountRing.IntegralDomain.type.
+check_join GRing.Zmodule.type CountRing.Ring.type CountRing.Ring.type.
+check_join GRing.Zmodule.type CountRing.UnitRing.type CountRing.UnitRing.type.
+check_join GRing.Zmodule.type CountRing.Zmodule.type CountRing.Zmodule.type.
+check_join GRing.Zmodule.type Countable.type CountRing.Zmodule.type.
+check_join GRing.Zmodule.type Equality.type GRing.Zmodule.type.
+check_join GRing.Zmodule.type Falgebra.type Falgebra.type.
+check_join GRing.Zmodule.type FieldExt.type FieldExt.type.
+check_join GRing.Zmodule.type FinGroup.type FinRing.Zmodule.type.
+check_join GRing.Zmodule.type FinRing.Algebra.type FinRing.Algebra.type.
+check_join GRing.Zmodule.type FinRing.ComRing.type FinRing.ComRing.type.
+check_join GRing.Zmodule.type FinRing.ComUnitRing.type FinRing.ComUnitRing.type.
+check_join GRing.Zmodule.type FinRing.Field.type FinRing.Field.type.
+check_join GRing.Zmodule.type FinRing.IntegralDomain.type FinRing.IntegralDomain.type.
+check_join GRing.Zmodule.type FinRing.Lalgebra.type FinRing.Lalgebra.type.
+check_join GRing.Zmodule.type FinRing.Lmodule.type FinRing.Lmodule.type.
+check_join GRing.Zmodule.type FinRing.Ring.type FinRing.Ring.type.
+check_join GRing.Zmodule.type FinRing.UnitAlgebra.type FinRing.UnitAlgebra.type.
+check_join GRing.Zmodule.type FinRing.UnitRing.type FinRing.UnitRing.type.
+check_join GRing.Zmodule.type FinRing.Zmodule.type FinRing.Zmodule.type.
+check_join GRing.Zmodule.type Finite.type FinRing.Zmodule.type.
+check_join GRing.Zmodule.type GRing.Algebra.type GRing.Algebra.type.
+check_join GRing.Zmodule.type GRing.ClosedField.type GRing.ClosedField.type.
+check_join GRing.Zmodule.type GRing.ComRing.type GRing.ComRing.type.
+check_join GRing.Zmodule.type GRing.ComUnitRing.type GRing.ComUnitRing.type.
+check_join GRing.Zmodule.type GRing.DecidableField.type GRing.DecidableField.type.
+check_join GRing.Zmodule.type GRing.Field.type GRing.Field.type.
+check_join GRing.Zmodule.type GRing.IntegralDomain.type GRing.IntegralDomain.type.
+check_join GRing.Zmodule.type GRing.Lalgebra.type GRing.Lalgebra.type.
+check_join GRing.Zmodule.type GRing.Lmodule.type GRing.Lmodule.type.
+check_join GRing.Zmodule.type GRing.Ring.type GRing.Ring.type.
+check_join GRing.Zmodule.type GRing.UnitAlgebra.type GRing.UnitAlgebra.type.
+check_join GRing.Zmodule.type GRing.UnitRing.type GRing.UnitRing.type.
+check_join GRing.Zmodule.type GRing.Zmodule.type GRing.Zmodule.type.
+check_join GRing.Zmodule.type Num.ArchimedeanField.type Num.ArchimedeanField.type.
+check_join GRing.Zmodule.type Num.ClosedField.type Num.ClosedField.type.
+check_join GRing.Zmodule.type Num.NumDomain.type Num.NumDomain.type.
+check_join GRing.Zmodule.type Num.NumField.type Num.NumField.type.
+check_join GRing.Zmodule.type Num.RealClosedField.type Num.RealClosedField.type.
+check_join GRing.Zmodule.type Num.RealDomain.type Num.RealDomain.type.
+check_join GRing.Zmodule.type Num.RealField.type Num.RealField.type.
+check_join GRing.Zmodule.type SplittingField.type SplittingField.type.
+check_join GRing.Zmodule.type Vector.type Vector.type.
+check_join Num.ArchimedeanField.type Choice.type Num.ArchimedeanField.type.
+check_join Num.ArchimedeanField.type Equality.type Num.ArchimedeanField.type.
+check_join Num.ArchimedeanField.type GRing.ComRing.type Num.ArchimedeanField.type.
+check_join Num.ArchimedeanField.type GRing.ComUnitRing.type Num.ArchimedeanField.type.
+check_join Num.ArchimedeanField.type GRing.Field.type Num.ArchimedeanField.type.
+check_join Num.ArchimedeanField.type GRing.IntegralDomain.type Num.ArchimedeanField.type.
+check_join Num.ArchimedeanField.type GRing.Ring.type Num.ArchimedeanField.type.
+check_join Num.ArchimedeanField.type GRing.UnitRing.type Num.ArchimedeanField.type.
+check_join Num.ArchimedeanField.type GRing.Zmodule.type Num.ArchimedeanField.type.
+check_join Num.ArchimedeanField.type Num.ArchimedeanField.type Num.ArchimedeanField.type.
+check_join Num.ArchimedeanField.type Num.NumDomain.type Num.ArchimedeanField.type.
+check_join Num.ArchimedeanField.type Num.NumField.type Num.ArchimedeanField.type.
+check_join Num.ArchimedeanField.type Num.RealDomain.type Num.ArchimedeanField.type.
+check_join Num.ArchimedeanField.type Num.RealField.type Num.ArchimedeanField.type.
+check_join Num.ClosedField.type Choice.type Num.ClosedField.type.
+check_join Num.ClosedField.type Equality.type Num.ClosedField.type.
+check_join Num.ClosedField.type GRing.ClosedField.type Num.ClosedField.type.
+check_join Num.ClosedField.type GRing.ComRing.type Num.ClosedField.type.
+check_join Num.ClosedField.type GRing.ComUnitRing.type Num.ClosedField.type.
+check_join Num.ClosedField.type GRing.DecidableField.type Num.ClosedField.type.
+check_join Num.ClosedField.type GRing.Field.type Num.ClosedField.type.
+check_join Num.ClosedField.type GRing.IntegralDomain.type Num.ClosedField.type.
+check_join Num.ClosedField.type GRing.Ring.type Num.ClosedField.type.
+check_join Num.ClosedField.type GRing.UnitRing.type Num.ClosedField.type.
+check_join Num.ClosedField.type GRing.Zmodule.type Num.ClosedField.type.
+check_join Num.ClosedField.type Num.ClosedField.type Num.ClosedField.type.
+check_join Num.ClosedField.type Num.NumDomain.type Num.ClosedField.type.
+check_join Num.ClosedField.type Num.NumField.type Num.ClosedField.type.
+check_join Num.NumDomain.type Choice.type Num.NumDomain.type.
+check_join Num.NumDomain.type Equality.type Num.NumDomain.type.
+check_join Num.NumDomain.type GRing.ClosedField.type Num.ClosedField.type.
+check_join Num.NumDomain.type GRing.ComRing.type Num.NumDomain.type.
+check_join Num.NumDomain.type GRing.ComUnitRing.type Num.NumDomain.type.
+check_join Num.NumDomain.type GRing.DecidableField.type Num.ClosedField.type.
+check_join Num.NumDomain.type GRing.Field.type Num.NumField.type.
+check_join Num.NumDomain.type GRing.IntegralDomain.type Num.NumDomain.type.
+check_join Num.NumDomain.type GRing.Ring.type Num.NumDomain.type.
+check_join Num.NumDomain.type GRing.UnitRing.type Num.NumDomain.type.
+check_join Num.NumDomain.type GRing.Zmodule.type Num.NumDomain.type.
+check_join Num.NumDomain.type Num.ArchimedeanField.type Num.ArchimedeanField.type.
+check_join Num.NumDomain.type Num.ClosedField.type Num.ClosedField.type.
+check_join Num.NumDomain.type Num.NumDomain.type Num.NumDomain.type.
+check_join Num.NumDomain.type Num.NumField.type Num.NumField.type.
+check_join Num.NumDomain.type Num.RealClosedField.type Num.RealClosedField.type.
+check_join Num.NumDomain.type Num.RealDomain.type Num.RealDomain.type.
+check_join Num.NumDomain.type Num.RealField.type Num.RealField.type.
+check_join Num.NumField.type Choice.type Num.NumField.type.
+check_join Num.NumField.type Equality.type Num.NumField.type.
+check_join Num.NumField.type GRing.ClosedField.type Num.ClosedField.type.
+check_join Num.NumField.type GRing.ComRing.type Num.NumField.type.
+check_join Num.NumField.type GRing.ComUnitRing.type Num.NumField.type.
+check_join Num.NumField.type GRing.DecidableField.type Num.ClosedField.type.
+check_join Num.NumField.type GRing.Field.type Num.NumField.type.
+check_join Num.NumField.type GRing.IntegralDomain.type Num.NumField.type.
+check_join Num.NumField.type GRing.Ring.type Num.NumField.type.
+check_join Num.NumField.type GRing.UnitRing.type Num.NumField.type.
+check_join Num.NumField.type GRing.Zmodule.type Num.NumField.type.
+check_join Num.NumField.type Num.ArchimedeanField.type Num.ArchimedeanField.type.
+check_join Num.NumField.type Num.ClosedField.type Num.ClosedField.type.
+check_join Num.NumField.type Num.NumDomain.type Num.NumField.type.
+check_join Num.NumField.type Num.NumField.type Num.NumField.type.
+check_join Num.NumField.type Num.RealClosedField.type Num.RealClosedField.type.
+check_join Num.NumField.type Num.RealDomain.type Num.RealField.type.
+check_join Num.NumField.type Num.RealField.type Num.RealField.type.
+check_join Num.RealClosedField.type Choice.type Num.RealClosedField.type.
+check_join Num.RealClosedField.type Equality.type Num.RealClosedField.type.
+check_join Num.RealClosedField.type GRing.ComRing.type Num.RealClosedField.type.
+check_join Num.RealClosedField.type GRing.ComUnitRing.type Num.RealClosedField.type.
+check_join Num.RealClosedField.type GRing.Field.type Num.RealClosedField.type.
+check_join Num.RealClosedField.type GRing.IntegralDomain.type Num.RealClosedField.type.
+check_join Num.RealClosedField.type GRing.Ring.type Num.RealClosedField.type.
+check_join Num.RealClosedField.type GRing.UnitRing.type Num.RealClosedField.type.
+check_join Num.RealClosedField.type GRing.Zmodule.type Num.RealClosedField.type.
+check_join Num.RealClosedField.type Num.NumDomain.type Num.RealClosedField.type.
+check_join Num.RealClosedField.type Num.NumField.type Num.RealClosedField.type.
+check_join Num.RealClosedField.type Num.RealClosedField.type Num.RealClosedField.type.
+check_join Num.RealClosedField.type Num.RealDomain.type Num.RealClosedField.type.
+check_join Num.RealClosedField.type Num.RealField.type Num.RealClosedField.type.
+check_join Num.RealDomain.type Choice.type Num.RealDomain.type.
+check_join Num.RealDomain.type Equality.type Num.RealDomain.type.
+check_join Num.RealDomain.type GRing.ComRing.type Num.RealDomain.type.
+check_join Num.RealDomain.type GRing.ComUnitRing.type Num.RealDomain.type.
+check_join Num.RealDomain.type GRing.Field.type Num.RealField.type.
+check_join Num.RealDomain.type GRing.IntegralDomain.type Num.RealDomain.type.
+check_join Num.RealDomain.type GRing.Ring.type Num.RealDomain.type.
+check_join Num.RealDomain.type GRing.UnitRing.type Num.RealDomain.type.
+check_join Num.RealDomain.type GRing.Zmodule.type Num.RealDomain.type.
+check_join Num.RealDomain.type Num.ArchimedeanField.type Num.ArchimedeanField.type.
+check_join Num.RealDomain.type Num.NumDomain.type Num.RealDomain.type.
+check_join Num.RealDomain.type Num.NumField.type Num.RealField.type.
+check_join Num.RealDomain.type Num.RealClosedField.type Num.RealClosedField.type.
+check_join Num.RealDomain.type Num.RealDomain.type Num.RealDomain.type.
+check_join Num.RealDomain.type Num.RealField.type Num.RealField.type.
+check_join Num.RealField.type Choice.type Num.RealField.type.
+check_join Num.RealField.type Equality.type Num.RealField.type.
+check_join Num.RealField.type GRing.ComRing.type Num.RealField.type.
+check_join Num.RealField.type GRing.ComUnitRing.type Num.RealField.type.
+check_join Num.RealField.type GRing.Field.type Num.RealField.type.
+check_join Num.RealField.type GRing.IntegralDomain.type Num.RealField.type.
+check_join Num.RealField.type GRing.Ring.type Num.RealField.type.
+check_join Num.RealField.type GRing.UnitRing.type Num.RealField.type.
+check_join Num.RealField.type GRing.Zmodule.type Num.RealField.type.
+check_join Num.RealField.type Num.ArchimedeanField.type Num.ArchimedeanField.type.
+check_join Num.RealField.type Num.NumDomain.type Num.RealField.type.
+check_join Num.RealField.type Num.NumField.type Num.RealField.type.
+check_join Num.RealField.type Num.RealClosedField.type Num.RealClosedField.type.
+check_join Num.RealField.type Num.RealDomain.type Num.RealField.type.
+check_join Num.RealField.type Num.RealField.type Num.RealField.type.
+check_join SplittingField.type Choice.type SplittingField.type.
+check_join SplittingField.type Equality.type SplittingField.type.
+check_join SplittingField.type Falgebra.type SplittingField.type.
+check_join SplittingField.type FieldExt.type SplittingField.type.
+check_join SplittingField.type GRing.Algebra.type SplittingField.type.
+check_join SplittingField.type GRing.ComRing.type SplittingField.type.
+check_join SplittingField.type GRing.ComUnitRing.type SplittingField.type.
+check_join SplittingField.type GRing.Field.type SplittingField.type.
+check_join SplittingField.type GRing.IntegralDomain.type SplittingField.type.
+check_join SplittingField.type GRing.Lalgebra.type SplittingField.type.
+check_join SplittingField.type GRing.Lmodule.type SplittingField.type.
+check_join SplittingField.type GRing.Ring.type SplittingField.type.
+check_join SplittingField.type GRing.UnitAlgebra.type SplittingField.type.
+check_join SplittingField.type GRing.UnitRing.type SplittingField.type.
+check_join SplittingField.type GRing.Zmodule.type SplittingField.type.
+check_join SplittingField.type SplittingField.type SplittingField.type.
+check_join SplittingField.type Vector.type SplittingField.type.
+check_join Vector.type Choice.type Vector.type.
+check_join Vector.type Equality.type Vector.type.
+check_join Vector.type Falgebra.type Falgebra.type.
+check_join Vector.type FieldExt.type FieldExt.type.
+check_join Vector.type GRing.Algebra.type Falgebra.type.
+check_join Vector.type GRing.ComRing.type FieldExt.type.
+check_join Vector.type GRing.ComUnitRing.type FieldExt.type.
+check_join Vector.type GRing.Field.type FieldExt.type.
+check_join Vector.type GRing.IntegralDomain.type FieldExt.type.
+check_join Vector.type GRing.Lalgebra.type Falgebra.type.
+check_join Vector.type GRing.Lmodule.type Vector.type.
+check_join Vector.type GRing.Ring.type Falgebra.type.
+check_join Vector.type GRing.UnitAlgebra.type Falgebra.type.
+check_join Vector.type GRing.UnitRing.type Falgebra.type.
+check_join Vector.type GRing.Zmodule.type Vector.type.
+check_join Vector.type SplittingField.type SplittingField.type.
+check_join Vector.type Vector.type Vector.type.
+Abort.