Fix some structures arguments (#1243)

src/Util/Structures/Equalities.v

@@ -2,6 +2,11 @@ Require Import Coq.Classes.Morphisms.
 Require Import Coq.Structures.Equalities.
 Require Export Crypto.Util.FixCoqMistakes.
 
+Module Type UsualEqualityTypeOrig <: EqualityTypeOrig
+ := UsualEq <+ UsualIsEqOrig.
+Module Type UsualEqualityTypeBoth <: EqualityTypeBoth
+ := UsualEq <+ UsualIsEq <+ UsualIsEqOrig.
+
 Local Coercion is_true : bool >-> Sortclass.
 Module Type IsEqb (Import E : Typ) (Import Eb:HasEqb E).
 #[global]

src/Util/Structures/Equalities/Bool.v

@@ -73,6 +73,8 @@ Module BoolBooleanDecidableType' := BoolBooleanDecidableType <+ EqNotation <+ Eq
 Module BoolDecidableTypeFull' := BoolDecidableTypeFull <+ EqNotation.
 
 Module BoolUsualEqualityType <: UsualEqualityType := BoolUsualEq <+ UsualIsEq.
+Module BoolUsualEqualityTypeOrig <: UsualEqualityTypeOrig := BoolUsualEq <+ UsualIsEqOrig.
+Module BoolUsualEqualityTypeBoth <: UsualEqualityTypeBoth := BoolUsualEq <+ UsualIsEq <+ UsualIsEqOrig.
 
 Module BoolUsualDecidableType <: UsualDecidableType
 := BoolUsualEq <+ UsualIsEq <+ BoolUsualHasEqDec.

src/Util/Structures/Equalities/Empty.v

@@ -81,6 +81,8 @@ Module EmptyBooleanDecidableType' := EmptyBooleanDecidableType <+ EqNotation <+
 Module EmptyDecidableTypeFull' := EmptyDecidableTypeFull <+ EqNotation.
 
 Module EmptyUsualEqualityType <: UsualEqualityType := EmptyUsualEq <+ UsualIsEq.
+Module EmptyUsualEqualityTypeOrig <: UsualEqualityTypeOrig := EmptyUsualEq <+ UsualIsEqOrig.
+Module EmptyUsualEqualityTypeBoth <: UsualEqualityTypeBoth := EmptyUsualEq <+ UsualIsEq <+ UsualIsEqOrig.
 
 Module EmptyUsualDecidableType <: UsualDecidableType
 := EmptyUsualEq <+ UsualIsEq <+ EmptyUsualHasEqDec.

src/Util/Structures/Equalities/List.v

@@ -67,9 +67,9 @@ End ListEqbSpec.
 
 Module ListHasEqBool (E : Eq) (Es : HasEqBool E) := ListHasEqb E Es <+ ListEqbSpec E E Es Es.
 
-Module ListUsualHasEqDec (E : UsualDecidableType).
+Module ListUsualHasEqDec (E : UsualEq) (EDec : HasEqDec E).
   Definition eq_dec (x y : list E.t) : {eq x y} + {~eq x y}
-    := List.list_eq_dec E.eq_dec x y.
+    := List.list_eq_dec EDec.eq_dec x y.
 End ListUsualHasEqDec.
 
 Module ListUsualEqbSpec (E : UsualBoolEq).
@@ -108,7 +108,7 @@ Module ListMiniDecidableType (E : MiniDecidableType) <: MiniDecidableType.
   Module Import _ListMiniDecidableType.
     Module E' := Make_UDT E.
   End _ListMiniDecidableType.
-  Include ListUsualHasEqDec E'.
+  Include ListUsualHasEqDec E' E'.
 End ListMiniDecidableType.
 
 Module ListUsualHasEqBool (E : UsualBoolEq) := ListHasEqb E E <+ ListUsualEqbSpec E.
@@ -136,17 +136,19 @@ Module ListBooleanDecidableType' (E : BooleanDecidableType) := ListBooleanDecida
 Module ListDecidableTypeFull' (E : DecidableTypeFull) := ListDecidableTypeFull E <+ EqNotation.
 
 Module ListUsualEqualityType (E : UsualEqualityType) <: UsualEqualityType := ListUsualEq E <+ UsualIsEq.
+Module ListUsualEqualityTypeOrig (E : UsualEqualityTypeOrig) <: UsualEqualityTypeOrig := ListUsualEq E <+ UsualIsEqOrig.
+Module ListUsualEqualityTypeBoth (E : UsualEqualityTypeBoth) <: UsualEqualityTypeBoth := ListUsualEq E <+ UsualIsEq <+ UsualIsEqOrig.
 
 Module ListUsualDecidableType (E : UsualDecidableType) <: UsualDecidableType
-:= ListUsualEq E <+ UsualIsEq <+ ListUsualHasEqDec E.
+:= ListUsualEq E <+ UsualIsEq <+ ListUsualHasEqDec E E.
 Module ListUsualDecidableTypeOrig (E : UsualDecidableType) <: UsualDecidableTypeOrig
-:= ListUsualEq E <+ UsualIsEqOrig <+ ListUsualHasEqDec E.
+:= ListUsualEq E <+ UsualIsEqOrig <+ ListUsualHasEqDec E E.
 Module ListUsualDecidableTypeBoth (E : UsualDecidableType) <: UsualDecidableTypeBoth
  := ListUsualDecidableType E <+ UsualIsEqOrig.
 Module ListUsualBoolEq (E : UsualBoolEq) <: UsualBoolEq
 := ListUsualEq E <+ ListUsualHasEqBool E.
 Module ListUsualDecidableTypeFull (E : UsualDecidableTypeFull) <: UsualDecidableTypeFull
- := ListUsualEq E <+ UsualIsEq <+ UsualIsEqOrig <+ ListUsualHasEqDec E <+ ListUsualHasEqBool E.
+ := ListUsualEq E <+ UsualIsEq <+ UsualIsEqOrig <+ ListUsualHasEqDec E E <+ ListUsualHasEqBool E.
 
 Local Coercion is_true : bool >-> Sortclass.
 Module ListIsEqb (E : EqbType).

src/Util/Structures/Equalities/Option.v

@@ -66,11 +66,11 @@ End OptionEqbSpec.
 
 Module OptionHasEqBool (E : Eq) (Es : HasEqBool E) := OptionHasEqb E Es <+ OptionEqbSpec E E Es Es.
 
-Module OptionUsualHasEqDec (E : UsualDecidableType).
+Module OptionUsualHasEqDec (E : UsualEq) (EDec : HasEqDec E).
   Definition eq_dec (x y : option E.t) : {eq x y} + {~eq x y}.
   Proof.
     destruct x as [x|], y as [y|];
-      [ destruct (E.eq_dec x y); [ left | right ]
+      [ destruct (EDec.eq_dec x y); [ left | right ]
       | right
       | right
       | left ];
@@ -120,7 +120,7 @@ Module OptionMiniDecidableType (E : MiniDecidableType) <: MiniDecidableType.
   Module Import _OptionMiniDecidableType.
     Module E' := Make_UDT E.
   End _OptionMiniDecidableType.
-  Include OptionUsualHasEqDec E'.
+  Include OptionUsualHasEqDec E' E'.
 End OptionMiniDecidableType.
 
 Local Coercion is_true : bool >-> Sortclass.
@@ -157,16 +157,18 @@ Module OptionBooleanDecidableType' (E : BooleanDecidableType) := OptionBooleanDe
 Module OptionDecidableTypeFull' (E : DecidableTypeFull) := OptionDecidableTypeFull E <+ EqNotation.
 
 Module OptionUsualEqualityType (E : UsualEqualityType) <: UsualEqualityType := OptionUsualEq E <+ UsualIsEq.
+Module OptionUsualEqualityTypeOrig (E : UsualEqualityTypeOrig) <: UsualEqualityTypeOrig := OptionUsualEq E <+ UsualIsEqOrig.
+Module OptionUsualEqualityTypeBoth (E : UsualEqualityTypeBoth) <: UsualEqualityTypeBoth := OptionUsualEq E <+ UsualIsEq <+ UsualIsEqOrig.
 
 Module OptionUsualDecidableType (E : UsualDecidableType) <: UsualDecidableType
-:= OptionUsualEq E <+ UsualIsEq <+ OptionUsualHasEqDec E.
-Module OptionUsualDecidableTypeOrig (E : UsualDecidableType) <: UsualDecidableTypeOrig
-:= OptionUsualEq E <+ UsualIsEqOrig <+ OptionUsualHasEqDec E.
-Module OptionUsualDecidableTypeBoth (E : UsualDecidableType) <: UsualDecidableTypeBoth
+:= OptionUsualEq E <+ UsualIsEq <+ OptionUsualHasEqDec E E.
+Module OptionUsualDecidableTypeOrig (E : UsualDecidableTypeOrig) <: UsualDecidableTypeOrig
+:= OptionUsualEq E <+ UsualIsEqOrig <+ OptionUsualHasEqDec E E.
+Module OptionUsualDecidableTypeBoth (E : UsualDecidableTypeBoth) <: UsualDecidableTypeBoth
  := OptionUsualDecidableType E <+ UsualIsEqOrig.
 Module OptionUsualBoolEq (E : UsualBoolEq) <: UsualBoolEq
 := OptionUsualEq E <+ OptionUsualHasEqBool E.
 Module OptionUsualDecidableTypeFull (E : UsualDecidableTypeFull) <: UsualDecidableTypeFull
- := OptionUsualEq E <+ UsualIsEq <+ UsualIsEqOrig <+ OptionUsualHasEqDec E <+ OptionUsualHasEqBool E.
+ := OptionUsualEq E <+ UsualIsEq <+ UsualIsEqOrig <+ OptionUsualHasEqDec E E <+ OptionUsualHasEqBool E.
 
 Module OptionEqbType (E : EqbType) <: EqbType := OptionTyp E <+ OptionHasEqb E E <+ OptionIsEqb E.

src/Util/Structures/Equalities/Prod.v

@@ -67,10 +67,10 @@ End ProdEqbSpec.
 
 Module ProdHasEqBool (E1 : Eq) (E2 : Eq) (E1s : HasEqBool E1) (E2s : HasEqBool E2) := ProdHasEqb E1 E2 E1s E2s <+ ProdEqbSpec E1 E2 E1 E2 E1s E2s E1s E2s.
 
-Module ProdUsualHasEqDec (E1 : UsualDecidableType) (E2 : UsualDecidableType).
+Module ProdUsualHasEqDec (E1 : UsualEq) (E2 : UsualEq) (E1Dec : HasEqDec E1) (E2Dec : HasEqDec E2).
   Definition eq_dec (x y : E1.t * E2.t) : {eq x y} + {~eq x y}.
   Proof.
-    destruct (E1.eq_dec (fst x) (fst y)); [ destruct (E2.eq_dec (snd x) (snd y)); [ left; destruct x, y | right; intro; subst y; destruct x ] | right; intro; subst y; destruct x ]; cbn in *; subst; try reflexivity; eauto using eq_refl with nocore.
+    destruct (E1Dec.eq_dec (fst x) (fst y)); [ destruct (E2Dec.eq_dec (snd x) (snd y)); [ left; destruct x, y | right; intro; subst y; destruct x ] | right; intro; subst y; destruct x ]; cbn in *; subst; try reflexivity; eauto using eq_refl with nocore.
   Defined.
 End ProdUsualHasEqDec.
 
@@ -112,7 +112,7 @@ Module ProdMiniDecidableType (E1 : MiniDecidableType) (E2 : MiniDecidableType) <
     Module E1' := Make_UDT E1.
     Module E2' := Make_UDT E2.
   End _ProdMiniDecidableType.
-  Include ProdUsualHasEqDec E1' E2'.
+  Include ProdUsualHasEqDec E1' E2' E1' E2'.
 End ProdMiniDecidableType.
 
 Local Coercion is_true : bool >-> Sortclass.
@@ -151,17 +151,19 @@ Module ProdBooleanEqualityType' (E1 : BooleanEqualityType) (E2 : BooleanEquality
 Module ProdBooleanDecidableType' (E1 : BooleanDecidableType) (E2 : BooleanDecidableType) := ProdBooleanDecidableType E1 E2 <+ EqNotation <+ EqbNotation.
 Module ProdDecidableTypeFull' (E1 : DecidableTypeFull) (E2 : DecidableTypeFull) := ProdDecidableTypeFull E1 E2 <+ EqNotation.
 
-Module ProdUsualEqualityType (E1 : UsualEqualityType) (E2 : UsualEqualityType) <: UsualEqualityType := ProdUsualEq E1 E2 <+ UsualIsEq.
+Module ProdUsualEqualityType (E1 : UsualEq) (E2 : UsualEq) <: UsualEqualityType := ProdUsualEq E1 E2 <+ UsualIsEq.
+Module ProdUsualEqualityTypeOrig (E1 : UsualEq) (E2 : UsualEq) <: UsualEqualityTypeOrig := ProdUsualEq E1 E2 <+ UsualIsEqOrig.
+Module ProdUsualEqualityTypeBoth (E1 : UsualEq) (E2 : UsualEq) <: UsualEqualityTypeBoth := ProdUsualEq E1 E2 <+ UsualIsEq <+ UsualIsEqOrig.
 
 Module ProdUsualDecidableType (E1 : UsualDecidableType) (E2 : UsualDecidableType) <: UsualDecidableType
-:= ProdUsualEq E1 E2 <+ UsualIsEq <+ ProdUsualHasEqDec E1 E2.
-Module ProdUsualDecidableTypeOrig (E1 : UsualDecidableType) (E2 : UsualDecidableType) <: UsualDecidableTypeOrig
-:= ProdUsualEq E1 E2 <+ UsualIsEqOrig <+ ProdUsualHasEqDec E1 E2.
-Module ProdUsualDecidableTypeBoth (E1 : UsualDecidableType) (E2 : UsualDecidableType) <: UsualDecidableTypeBoth
+:= ProdUsualEq E1 E2 <+ UsualIsEq <+ ProdUsualHasEqDec E1 E2 E1 E2.
+Module ProdUsualDecidableTypeOrig (E1 : UsualDecidableTypeOrig) (E2 : UsualDecidableTypeOrig) <: UsualDecidableTypeOrig
+:= ProdUsualEq E1 E2 <+ UsualIsEqOrig <+ ProdUsualHasEqDec E1 E2 E1 E2.
+Module ProdUsualDecidableTypeBoth (E1 : UsualDecidableTypeBoth) (E2 : UsualDecidableTypeBoth) <: UsualDecidableTypeBoth
  := ProdUsualDecidableType E1 E2 <+ UsualIsEqOrig.
 Module ProdUsualBoolEq (E1 : UsualBoolEq) (E2 : UsualBoolEq) <: UsualBoolEq
 := ProdUsualEq E1 E2 <+ ProdUsualHasEqBool E1 E2.
 Module ProdUsualDecidableTypeFull (E1 : UsualDecidableTypeFull) (E2 : UsualDecidableTypeFull) <: UsualDecidableTypeFull
- := ProdUsualEq E1 E2 <+ UsualIsEq <+ UsualIsEqOrig <+ ProdUsualHasEqDec E1 E2 <+ ProdUsualHasEqBool E1 E2.
+ := ProdUsualEq E1 E2 <+ UsualIsEq <+ UsualIsEqOrig <+ ProdUsualHasEqDec E1 E2 E1 E2 <+ ProdUsualHasEqBool E1 E2.
 
 Module ProdEqbType (E1 : EqbType) (E2 : EqbType) <: EqbType := ProdTyp E1 E2 <+ ProdHasEqb E1 E2 E1 E2 <+ ProdIsEqb E1 E2.

src/Util/Structures/Equalities/Sum.v

@@ -67,14 +67,14 @@ End SumEqbSpec.
 
 Module SumHasEqBool (E1 : Eq) (E2 : Eq) (E1s : HasEqBool E1) (E2s : HasEqBool E2) := SumHasEqb E1 E2 E1s E2s <+ SumEqbSpec E1 E2 E1 E2 E1s E2s E1s E2s.
 
-Module SumUsualHasEqDec (E1 : UsualDecidableType) (E2 : UsualDecidableType).
+Module SumUsualHasEqDec (E1 : UsualEq) (E2 : UsualEq) (E1Dec : HasEqDec E1) (E2Dec : HasEqDec E2).
   Definition eq_dec (x y : E1.t + E2.t) : {eq x y} + {~eq x y}.
   Proof.
     destruct x as [x|x], y as [y|y];
-      [ destruct (E1.eq_dec x y); [ left | right ]
+      [ destruct (E1Dec.eq_dec x y); [ left | right ]
       | right
       | right
-      | destruct (E2.eq_dec x y); [ left | right ] ];
+      | destruct (E2Dec.eq_dec x y); [ left | right ] ];
       repeat first [ apply f_equal
                    | assumption
                    | intro
@@ -121,7 +121,7 @@ Module SumMiniDecidableType (E1 : MiniDecidableType) (E2 : MiniDecidableType) <:
     Module E1' := Make_UDT E1.
     Module E2' := Make_UDT E2.
   End _SumMiniDecidableType.
-  Include SumUsualHasEqDec E1' E2'.
+  Include SumUsualHasEqDec E1' E2' E1' E2'.
 End SumMiniDecidableType.
 
 Local Coercion is_true : bool >-> Sortclass.
@@ -157,17 +157,19 @@ Module SumBooleanEqualityType' (E1 : BooleanEqualityType) (E2 : BooleanEqualityT
 Module SumBooleanDecidableType' (E1 : BooleanDecidableType) (E2 : BooleanDecidableType) := SumBooleanDecidableType E1 E2 <+ EqNotation <+ EqbNotation.
 Module SumDecidableTypeFull' (E1 : DecidableTypeFull) (E2 : DecidableTypeFull) := SumDecidableTypeFull E1 E2 <+ EqNotation.
 
-Module SumUsualEqualityType (E1 : UsualEqualityType) (E2 : UsualEqualityType) <: UsualEqualityType := SumUsualEq E1 E2 <+ UsualIsEq.
+Module SumUsualEqualityType (E1 : UsualEq) (E2 : UsualEq) <: UsualEqualityType := SumUsualEq E1 E2 <+ UsualIsEq.
+Module SumUsualEqualityTypeOrig (E1 : UsualEq) (E2 : UsualEq) <: UsualEqualityTypeOrig := SumUsualEq E1 E2 <+ UsualIsEqOrig.
+Module SumUsualEqualityTypeBoth (E1 : UsualEq) (E2 : UsualEq) <: UsualEqualityTypeBoth := SumUsualEq E1 E2 <+ UsualIsEq <+ UsualIsEqOrig.
 
 Module SumUsualDecidableType (E1 : UsualDecidableType) (E2 : UsualDecidableType) <: UsualDecidableType
-:= SumUsualEq E1 E2 <+ UsualIsEq <+ SumUsualHasEqDec E1 E2.
-Module SumUsualDecidableTypeOrig (E1 : UsualDecidableType) (E2 : UsualDecidableType) <: UsualDecidableTypeOrig
-:= SumUsualEq E1 E2 <+ UsualIsEqOrig <+ SumUsualHasEqDec E1 E2.
-Module SumUsualDecidableTypeBoth (E1 : UsualDecidableType) (E2 : UsualDecidableType) <: UsualDecidableTypeBoth
+:= SumUsualEq E1 E2 <+ UsualIsEq <+ SumUsualHasEqDec E1 E2 E1 E2.
+Module SumUsualDecidableTypeOrig (E1 : UsualDecidableTypeOrig) (E2 : UsualDecidableTypeOrig) <: UsualDecidableTypeOrig
+:= SumUsualEq E1 E2 <+ UsualIsEqOrig <+ SumUsualHasEqDec E1 E2 E1 E2.
+Module SumUsualDecidableTypeBoth (E1 : UsualDecidableTypeBoth) (E2 : UsualDecidableTypeBoth) <: UsualDecidableTypeBoth
  := SumUsualDecidableType E1 E2 <+ UsualIsEqOrig.
 Module SumUsualBoolEq (E1 : UsualBoolEq) (E2 : UsualBoolEq) <: UsualBoolEq
 := SumUsualEq E1 E2 <+ SumUsualHasEqBool E1 E2.
 Module SumUsualDecidableTypeFull (E1 : UsualDecidableTypeFull) (E2 : UsualDecidableTypeFull) <: UsualDecidableTypeFull
- := SumUsualEq E1 E2 <+ UsualIsEq <+ UsualIsEqOrig <+ SumUsualHasEqDec E1 E2 <+ SumUsualHasEqBool E1 E2.
+ := SumUsualEq E1 E2 <+ UsualIsEq <+ UsualIsEqOrig <+ SumUsualHasEqDec E1 E2 E1 E2 <+ SumUsualHasEqBool E1 E2.
 
 Module SumEqbType (E1 : EqbType) (E2 : EqbType) <: EqbType := SumTyp E1 E2 <+ SumHasEqb E1 E2 E1 E2 <+ SumIsEqb E1 E2.

src/Util/Structures/Equalities/Unit.v

@@ -82,6 +82,8 @@ Module UnitBooleanDecidableType' := UnitBooleanDecidableType <+ EqNotation <+ Eq
 Module UnitDecidableTypeFull' := UnitDecidableTypeFull <+ EqNotation.
 
 Module UnitUsualEqualityType <: UsualEqualityType := UnitUsualEq <+ UsualIsEq.
+Module UnitUsualEqualityTypeOrig <: UsualEqualityTypeOrig := UnitUsualEq <+ UsualIsEqOrig.
+Module UnitUsualEqualityTypeBoth <: UsualEqualityTypeBoth := UnitUsualEq <+ UsualIsEq <+ UsualIsEqOrig.
 
 Module UnitUsualDecidableType <: UsualDecidableType
 := UnitUsualEq <+ UsualIsEq <+ UnitUsualHasEqDec.

src/Util/Structures/Orders/List.v

@@ -428,7 +428,7 @@ Module ListUsualStrOrder (E : UsualStrOrder) <: UsualStrOrder := ListUsualEquali
 Module ListUsualHasCompare (E : UsualEqLt) (Ec : HasCompare E) := ListHasCmp E Ec <+ ListUsualCmpSpec E Ec.
 
 Module ListUsualDecStrOrder (E : UsualDecStrOrder) <: UsualDecStrOrder := ListUsualStrOrder E <+ ListUsualHasCompare E E.
-Module ListUsualOrderedType (E : UsualOrderedType) <: UsualOrderedType := ListUsualDecStrOrder E <+ ListUsualHasEqDec E.
+Module ListUsualOrderedType (E : UsualOrderedType) <: UsualOrderedType := ListUsualDecStrOrder E <+ ListUsualHasEqDec E E.
 Module ListUsualOrderedTypeFull (E : UsualOrderedTypeFull) <: UsualOrderedTypeFull := ListUsualOrderedType E <+ ListHasLe E <+ ListUsualLeIsLtEq E E E.
 
 Module ListUsualStrOrder' (E : UsualStrOrder) <: UsualStrOrder' := ListUsualStrOrder E <+ LtNotation.

src/Util/Structures/Orders/Option.v

@@ -323,7 +323,7 @@ Module OptionUsualStrOrder (E : UsualStrOrder) <: UsualStrOrder := OptionUsualEq
 Module OptionUsualHasCompare (E : UsualEqLt) (Ec : HasCompare E) := OptionHasCmp E Ec <+ OptionUsualCmpSpec E Ec.
 
 Module OptionUsualDecStrOrder (E : UsualDecStrOrder) <: UsualDecStrOrder := OptionUsualStrOrder E <+ OptionUsualHasCompare E E.
-Module OptionUsualOrderedType (E : UsualOrderedType) <: UsualOrderedType := OptionUsualDecStrOrder E <+ OptionUsualHasEqDec E.
+Module OptionUsualOrderedType (E : UsualOrderedType) <: UsualOrderedType := OptionUsualDecStrOrder E <+ OptionUsualHasEqDec E E.
 Module OptionUsualOrderedTypeFull (E : UsualOrderedTypeFull) <: UsualOrderedTypeFull := OptionUsualOrderedType E <+ OptionHasLe E <+ OptionUsualLeIsLtEq E E E.
 
 Module OptionUsualStrOrder' (E : UsualStrOrder) <: UsualStrOrder' := OptionUsualStrOrder E <+ LtNotation.

src/Util/Structures/Orders/Prod.v

@@ -418,7 +418,7 @@ Module ProdUsualStrOrder (E1 : UsualStrOrder) (E2 : UsualStrOrder) <: UsualStrOr
 Module ProdUsualHasCompare (E1 : UsualEqLt) (E2 : UsualEqLt) (E1c : HasCompare E1) (E2c : HasCompare E2) := ProdHasCmp E1 E2 E1c E2c <+ ProdUsualCmpSpec E1 E2 E1c E2c.
 
 Module ProdUsualDecStrOrder (E1 : UsualDecStrOrder) (E2 : UsualDecStrOrder) <: UsualDecStrOrder := ProdUsualStrOrder E1 E2 <+ ProdUsualHasCompare E1 E2 E1 E2.
-Module ProdUsualOrderedType (E1 : UsualOrderedType) (E2 : UsualOrderedType) <: UsualOrderedType := ProdUsualDecStrOrder E1 E2 <+ ProdUsualHasEqDec E1 E2.
+Module ProdUsualOrderedType (E1 : UsualOrderedType) (E2 : UsualOrderedType) <: UsualOrderedType := ProdUsualDecStrOrder E1 E2 <+ ProdUsualHasEqDec E1 E2 E1 E2.
 Module ProdUsualOrderedTypeFull (E1 : UsualOrderedTypeFull) (E2 : UsualOrderedTypeFull) <: UsualOrderedTypeFull := ProdUsualOrderedType E1 E2 <+ ProdHasLe E1 E2 <+ ProdUsualLeIsLtEq E1 E2 E1 E2 E1.
 
 Module ProdUsualStrOrder' (E1 : UsualStrOrder) (E2 : UsualStrOrder) <: UsualStrOrder' := ProdUsualStrOrder E1 E2 <+ LtNotation.
@@ -523,36 +523,3 @@ Module ProdBoolOrdSpecs (O1 : EqLtLe) (O2 : EqLtLe) (F1 : HasBoolOrdFuns O1) (F2
 Module ProdOrderFunctions (O1 : EqLtLe) (O2 : EqLtLe) (F1 : OrderFunctions O1) (F2 : OrderFunctions O2) (O1e : IsEq O1) := ProdHasCompare O1 O2 F1 F2 O1e <+ ProdHasBoolOrdFuns O1 O2 F1 F2 <+ ProdBoolOrdSpecs O1 O2 F1 F2 F1 F2.
 
 Module ProdOrderFunctions' (O1 : EqLtLe) (O2 : EqLtLe) (F1 : OrderFunctions O1) (F2 : OrderFunctions O2) (O1e : IsEq O1) := ProdHasCompare O1 O2 F1 F2 O1e <+ ProdCmpNotation O1 O2 F1 F2 <+ ProdHasBoolOrdFuns' O1 O2 F1 F2 <+ ProdBoolOrdSpecs O1 O2 F1 F2 F1 F2.
-
-
-
-
-
-
-
-
-
-
-
-
-(*
-Module ProdTotalLeBool (E1 : CompatibleTotalEqLtLeBool) (E2 : TotalLeBool) <: TotalLeBool := ProdLeBool E1 E2 <+ ProdLebIsTotal E1 E2 E1 E2 E1 E1.
-Module ProdTotalLeBool' (E1 : TotalLeBool) (E2 : TotalLeBool) <: TotalLeBool' := ProdLeBool' E1 E2 <+ ProdLebIsTotal E1 E2.
-Module ProdTotalEqLtLeBool (E1 : TotalEqLtLeBool) (E2 : TotalEqLtLeBool) <: TotalEqLtLeBool := ProdEqLtLeBool E1 E2 <+ ProdEqLtLebIsTotal E1 E2.
-Module ProdTotalEqLtLeBool' (E1 : TotalEqLtLeBool) (E2 : TotalEqLtLeBool) <: TotalEqLtLeBool' := ProdEqLtLeBool' E1 E2 <+ ProdEqLtLebIsTotal E1 E2.
-
-Module ProdTotalTransitiveLeBool (E1 : TotalTransitiveLeBool) (E2 : TotalTransitiveLeBool) <: TotalTransitiveLeBool := ProdTotalLeBool E1 E2 <+ ProdLebIsTransitive E1 E2 E1 E2.
-Module ProdTotalTransitiveLeBool' (E1 : TotalTransitiveLeBool) (E2 : TotalTransitiveLeBool) <: TotalTransitiveLeBool' := ProdTotalLeBool' E1 E2 <+ ProdLebIsTransitive E1 E2 E1 E2.
-
-Module ProdHasBoolOrdFuns (E1 : Typ) (E2 : Typ) (E1s : HasBoolOrdFuns E1) (E2s : HasBoolOrdFuns E2) := ProdTyp E1 E2 <+ ProdHasEqb E1 E2 E1s E2s <+ ProdHasLtb E1 E2 E1s E2s <+ ProdHasLeb E1 E2 E1s E2s.
-
-Module ProdHasBoolOrdFuns' (E1 : Typ) (E2 : Typ) (E1s : HasBoolOrdFuns E1) (E2s : HasBoolOrdFuns E2) := ProdHasBoolOrdFuns E1 E2 E1s E2s <+ ProdEqbNotation E1 E2 E1s E2s <+ ProdLtbNotation E1 E2 E1s E2s <+ ProdLebNotation E1 E2 E1s E2s.
-
-Module ProdBoolOrdSpecs (E1 : EqLtLe) (E2 : EqLtLe) (F1 : HasBoolOrdFuns E1) (F2 : HasBoolOrdFuns E2) (E1s : BoolOrdSpecs E1 F1) (E2s : BoolOrdSpecs E2 F2)
-:= ProdEqbSpec E1 E2 E1 E2 F1 F2 E1s E2s <+ ProdLtbSpec E1 E2 E1 E2 F1 F2 E1s E2s <+ ProdLebSpec E1 E2 E1 E2 F1 F2 E1s E2s.
-
-Module ProdOrderFunctions (E1 : EqLtLe) (E2 : EqLtLe) (E1f : OrderFunctions E1) (E2f : OrderFunctions E2)
-:= ProdHasCompare E1 E2 E1f E2f <+ ProdHasBoolOrdFuns E1 E2 E1f E2f <+ ProdBoolOrdSpecs E1 E2 E1f E2f E1f E2f.
-Module ProdOrderFunctions' (E1 : EqLtLe) (E2 : EqLtLe) (E1f : OrderFunctions E1) (E2f : OrderFunctions E2)
-:= ProdHasCompare E1 E2 E1f E2f <+ ProdCmpNotation E1 E2 E1f E2f <+ ProdHasBoolOrdFuns' E1 E2 E1f E2f <+ ProdBoolOrdSpecs E1 E2 E1f E2f E1f E2f.
-*)