`in11(1)_sig` subsumes `in(2|3)_sig`

2 files changed, 18 insertions, 21 deletions

diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v
index f4ecfbb..d99dedf 100644
--- a/mathcomp/ssreflect/path.v
+++ b/mathcomp/ssreflect/path.v
@@ -882,7 +882,7 @@ Arguments sort_map {T T' f leT}.
 Section SortSeq_in.
 
 Variables (T : Type) (P : {pred T}) (leT : rel T).
-Notation le_sT := (relpre (val : sig P -> _) leT).
+Let le_sT := relpre (val : sig P -> _) leT.
 
 Hypothesis leT_total : {in P &, total leT}.
 Let le_sT_total : total le_sT := in2_sig leT_total.
@@ -1138,7 +1138,7 @@ Variables (T : Type) (P : {pred T}) (leT : rel T).
 Hypothesis leT_total : {in P &, total leT}.
 Hypothesis leT_tr : {in P & &, transitive leT}.
 
-Notation le_sT := (relpre (val : sig P -> _) leT).
+Let le_sT := relpre (val : sig P -> _) leT.
 Let le_sT_total : total le_sT := in2_sig leT_total.
 Let le_sT_tr : transitive le_sT := in3_sig leT_tr.
 
diff --git a/mathcomp/ssreflect/ssrbool.v b/mathcomp/ssreflect/ssrbool.v
index 1864b53..49be7b0 100644
--- a/mathcomp/ssreflect/ssrbool.v
+++ b/mathcomp/ssreflect/ssrbool.v
@@ -102,6 +102,10 @@ Arguments mono_sym_in {aT rT} [aR rR f aD].
 Arguments homo_sym_in11 {aT rT} [aR rR f aD aD'].
 Arguments mono_sym_in11 {aT rT} [aR rR f aD aD'].
 
+(******************)
+(* v8.14 addtions *)
+(******************)
+
 Section LocalGlobal.
 
 Local Notation "{ 'all1' P }" := (forall x, P x : Prop) (at level 0).
@@ -209,6 +213,10 @@ Arguments in_on1S  {T1 T2} D2 {f Q1}.
 Arguments in_on1lS {T1 T2 T3} D2 {f h Q1l}.
 Arguments in_on2S  {T1 T2} D2 {f Q2}.
 
+(******************)
+(* v8.13 addtions *)
+(******************)
+
 Section CancelOn.
 
 Variables (aT rT : predArgType) (aD : {pred aT}) (rD : {pred rT}).
@@ -362,32 +370,21 @@ Local Notation "{ 'all3' P }" := (forall x y z, P x y z : Prop) (at level 0).
 Variables T1 T2 T3 : Type.
 Variables (D1 : {pred T1}) (D2 : {pred T2})  (D3 : {pred T3}).
 Variable P1 : T1 -> Prop.
-Variable P11 : T1 -> T2 -> Prop.
-Variable P111 : T1 -> T2 -> T3 -> Prop.
-Variable P2 :  T1 -> T1 -> Prop.
-Variable P3 :  T1 -> T1 -> T1 -> Prop.
+Variable P2 : T1 -> T2 -> Prop.
+Variable P3 : T1 -> T2 -> T3 -> Prop.
 
 Lemma in1_sig : {in D1, {all1 P1}} -> forall x : sig D1, P1 (sval x).
 Proof. by move=> DP [x Dx]; have := DP _ Dx. Qed.
 
-Lemma in11_sig : {in D1 & D2, {all2 P11}} ->
-  forall (x : sig D1) (y : sig D2), P11 (sval x) (sval y).
-Proof. by move=> DP [x Dx] [y Dy]; have := DP _ _ Dx Dy. Qed.
-
-Lemma in111_sig : {in D1 & D2 & D3, {all3 P111}} ->
-  forall (x : sig D1) (y : sig D2) (z : sig D3), P111 (sval x) (sval y) (sval z).
-Proof. by move=> DP [x Dx] [y Dy] [z Dz]; have := DP _ _ _ Dx Dy Dz. Qed.
-
-Lemma in2_sig : {in D1 &, {all2 P2}} -> forall x y : sig D1, P2 (sval x) (sval y).
+Lemma in2_sig : {in D1 & D2, {all2 P2}} ->
+  forall (x : sig D1) (y : sig D2), P2 (sval x) (sval y).
 Proof. by move=> DP [x Dx] [y Dy]; have := DP _ _ Dx Dy. Qed.
 
-Lemma in3_sig : {in D1 & &, {all3 P3}} ->
-   forall x y z : sig D1, P3 (sval x) (sval y) (sval z).
+Lemma in3_sig : {in D1 & D2 & D3, {all3 P3}} ->
+  forall (x : sig D1) (y : sig D2) (z : sig D3), P3 (sval x) (sval y) (sval z).
 Proof. by move=> DP [x Dx] [y Dy] [z Dz]; have := DP _ _ _ Dx Dy Dz. Qed.
 
 End in_sig.
 Arguments in1_sig {T1 D1 P1}.
-Arguments in11_sig {T1 T2 D1 D2 P11}.
-Arguments in111_sig {T1 T2 T3 D1 D2 D3 P111}.
-Arguments in2_sig {T1 D1 P2}.
-Arguments in3_sig {T1 D1 P3}.
+Arguments in2_sig {T1 T2 D1 D2 P2}.
+Arguments in3_sig {T1 T2 T3 D1 D2 D3 P3}.