From bfd6750cce611d2ae31aeb2fca8df9b769b7f0e9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Sun, 9 Mar 2025 10:28:54 +0100
Subject: [PATCH] Change order of some conj and disj. Rename insertF_inj_l <->
 insertF_inj_r,        insertF_nextF_compat_l <-> insertF_nextF_compat_r,     
   insert2F_inj_l -> insert2F_inj_r,        insert2F_inj_r{0,1} ->
 insert2F_inj_l{0,1},        insert2F_nextF_compat_l ->
 insert2F_nextF_compat_r,        insert2F_nextF_compat_r{0,1} ->
 insert2F_nextF_compat_l{0,1},        replaceF_reg_l <-> replaceF_reg_r,      
  replaceF_neqxF_compat_l <-> replaceF_neqxF_compat_r,        replace2F_reg_l
 -> replace2F_reg_r,        replace2F_reg_r{0,1} -> replace2F_reg_l{0,1},     
   insertT{r,c,}_inj_l <-> insertT{r,c,}_inj_r,       
 insertT{r,c,}_nextT_compat_l <-> insertT{r,c,}_nextT_compat_r,       
 replaceT{r,c,}_reg_l <-> replaceT{r,c,}_reg_r,       
 replaceT{r,c,}_neqxT{r,c,}_compat_l <-> replaceT{r,c,}_neqxT{r,c,}_compat_r, 
       {insertF,replaceF}_zero_reg_l <-> {insertF,replaceF}_zero_reg_r,       
 {insert2F,replace2F}_zero_reg_l -> {insert2F,replace2F}_zero_reg_r,       
 {insert2F,replace2F}_zero_reg_r{0,1} -> {insert2F,replace2F}_zero_reg_l{0,1},
        {insertT,replaceT}{r,c,}_zero_reg_l <->
 {insertT,replaceT}{r,c,}_zero_reg_r,

---
 Algebra/Monoid/Monoid_FF.v | 124 +++++++++++++-------------
 Algebra/Monoid/Monoid_FT.v |  58 ++++++------
 Subsets/Finite_family.v    | 176 ++++++++++++++++++-------------------
 Subsets/Finite_table.v     | 144 +++++++++++++++---------------
 4 files changed, 251 insertions(+), 251 deletions(-)

diff --git a/Algebra/Monoid/Monoid_FF.v b/Algebra/Monoid/Monoid_FF.v
index edf97182..32893d15 100644
--- a/Algebra/Monoid/Monoid_FF.v
+++ b/Algebra/Monoid/Monoid_FF.v
@@ -655,34 +655,34 @@ Lemma concatF_zero_nextF_compat_r :
 Proof. move=>>; rewrite -concatF_zero; apply concatF_nextF_compat_r. Qed.
 
 Lemma insertF_zero_compat :
-  forall {n} (A : 'G^n) x0 i0, A = 0 -> x0 = 0 -> insertF i0 x0 A = 0.
+  forall {n} i0 x0 (A : 'G^n), x0 = 0 -> A = 0 -> insertF i0 x0 A = 0.
 Proof. move=>> HA H0; rewrite HA H0; apply insertF_zero. Qed.
 
 Lemma insert2F_zero_compat :
-  forall {n} (A : 'G^n) x0 x1 {i0 i1} (H : i1 <> i0),
-    A = 0 -> x0 = 0 -> x1 = 0 -> insert2F H x0 x1 A = 0.
+  forall {n} {i0 i1} (H : i1 <> i0) x0 x1 (A : 'G^n),
+    x0 = 0 -> x1 = 0 ->  A = 0 ->insert2F H x0 x1 A = 0.
 Proof. move=>> HA H0 H1; rewrite HA H0 H1; apply insert2F_zero. Qed.
 
 Lemma skipF_zero_compat :
-  forall {n} (A : 'G^n.+1) i0, eqxF i0 A 0  -> skipF i0 A = 0.
+  forall {n} i0 (A : 'G^n.+1), eqxF i0 A 0  -> skipF i0 A = 0.
 Proof.
 move=>> H; erewrite <- skipF_zero; apply skipF_eq; try apply H; easy.
 Qed.
 
 Lemma skip2F_zero_compat :
-  forall {n} (A : 'G^n.+2) {i0 i1 : 'I_n.+2} (H : i1 <> i0),
+  forall {n} {i0 i1 : 'I_n.+2} (H : i1 <> i0) (A : 'G^n.+2),
     eqx2F i0 i1 A 0 -> skip2F H A = 0.
 Proof.
-intros n A i0 i1 H HA; rewrite -(skip2F_zero H); apply skip2F_eq; easy.
+intros n i0 i1 H A HA; rewrite -(skip2F_zero H); apply skip2F_eq; easy.
 Qed.
 
 Lemma replaceF_zero_compat :
-  forall {n} (A : 'G^n) x0 i0, eqxF i0 A 0  -> x0 = 0 -> replaceF i0 x0 A = 0.
+  forall {n} i0 x0 (A : 'G^n), x0 = 0 -> eqxF i0 A 0 -> replaceF i0 x0 A = 0.
 Proof. intros; erewrite <- replaceF_zero; apply replaceF_eq; easy. Qed.
 
 Lemma replace2F_zero_compat :
-  forall {n} (A : 'G^n) x0 x1 i0 i1,
-    eqx2F i0 i1 A 0 -> x0 = 0 -> x1 = 0 -> replace2F i0 i1 x0 x1 A = 0.
+  forall {n} i0 i1 x0 x1 (A : 'G^n),
+    x0 = 0 -> x1 = 0 -> eqx2F i0 i1 A 0 -> replace2F i0 i1 x0 x1 A = 0.
 Proof. intros; erewrite <- replace2F_zero; apply replace2F_eq; easy. Qed.
 
 Lemma mapF_zero_compat :
@@ -752,67 +752,67 @@ Lemma concatF_zero_nextF_reg :
 Proof. move=>>; rewrite -concatF_zero; apply concatF_nextF_reg. Qed.
 
 Lemma insertF_zero_reg_l :
-  forall {n} (A : 'G^n) x0 i0, insertF i0 x0 A = 0 -> A = 0.
+  forall {n} i0 x0 (A : 'G^n), insertF i0 x0 A = 0 -> x0 = 0.
 Proof. move=>>; erewrite <- insertF_zero; apply insertF_inj_l. Qed.
 
 Lemma insertF_zero_reg_r :
-  forall {n} (A : 'G^n) x0 i0, insertF i0 x0 A = 0 -> x0 = 0.
+  forall {n} i0 x0 (A : 'G^n), insertF i0 x0 A = 0 -> A = 0.
 Proof. move=>>; erewrite <- insertF_zero; apply insertF_inj_r. Qed.
 
-Lemma insert2F_zero_reg_l :
-  forall {n} (A : 'G^n) x0 x1 {i0 i1} (H : i1 <> i0),
-    insert2F H x0 x1 A = 0 -> A = 0.
-Proof. move=>>; erewrite <- insert2F_zero; apply insert2F_inj_l. Qed.
-
-Lemma insert2F_zero_reg_r0 :
-  forall {n} (A : 'G^n) x0 x1 {i0 i1} (H : i1 <> i0),
+Lemma insert2F_zero_reg_l0 :
+  forall {n} {i0 i1} (H : i1 <> i0) x0 x1 (A : 'G^n),
     insert2F H x0 x1 A = 0 -> x0 = 0.
-Proof. move=>>; erewrite <- insert2F_zero; apply insert2F_inj_r0. Qed.
+Proof. move=>>; erewrite <- insert2F_zero; apply insert2F_inj_l0. Qed.
 
-Lemma insert2F_zero_reg_r1 :
-  forall {n} (A : 'G^n) x0 x1 {i0 i1} (H : i1 <> i0),
+Lemma insert2F_zero_reg_l1 :
+  forall {n} {i0 i1} (H : i1 <> i0) x0 x1 (A : 'G^n),
     insert2F H x0 x1 A = 0 -> x1 = 0.
-Proof. move=>>; erewrite <- insert2F_zero; apply insert2F_inj_r1. Qed.
+Proof. move=>>; erewrite <- insert2F_zero; apply insert2F_inj_l1. Qed.
+
+Lemma insert2F_zero_reg_r :
+  forall {n} {i0 i1} (H : i1 <> i0) x0 x1 (A : 'G^n),
+    insert2F H x0 x1 A = 0 -> A = 0.
+Proof. move=>>; erewrite <- insert2F_zero; apply insert2F_inj_r. Qed.
 
 Lemma skipF_zero_reg :
-  forall {n} (A : 'G^n.+1) i0, skipF i0 A = 0 -> eqxF i0 A 0 .
+  forall {n} i0 (A : 'G^n.+1), skipF i0 A = 0 -> eqxF i0 A 0 .
 Proof. move=>>; erewrite <- skipF_zero; apply skipF_reg. Qed.
 
 Lemma skip2F_zero_reg :
-  forall {n} (A : 'G^n.+2) {i0 i1} (H : i1 <> i0),
+  forall {n} {i0 i1} (H : i1 <> i0) (A : 'G^n.+2),
     skip2F H A = 0 -> eqx2F i0 i1 A 0.
 Proof. move=>>; erewrite <- skip2F_zero; apply skip2F_reg. Qed.
 
 Lemma replaceF_zero_reg_l :
-  forall {n} (A : 'G^n) x0 i0, replaceF i0 x0 A = 0 -> eqxF i0 A 0 .
+  forall {n} i0 x0 (A : 'G^n), replaceF i0 x0 A = 0 -> x0 = 0.
 Proof. move=>>; erewrite <- replaceF_zero at 1; apply replaceF_reg_l. Qed.
 
 Lemma replaceF_zero_reg_r :
-  forall {n} (A : 'G^n) x0 i0, replaceF i0 x0 A = 0 -> x0 = 0.
+  forall {n} i0 x0 (A : 'G^n), replaceF i0 x0 A = 0 -> eqxF i0 A 0 .
 Proof. move=>>; erewrite <- replaceF_zero at 1; apply replaceF_reg_r. Qed.
 
 Lemma replaceF_zero_reg :
-  forall {n} (A : 'G^n) x0 i0, replaceF i0 x0 A = 0 -> eqxF i0 A 0  /\ x0 = 0.
+  forall {n} i0 x0 (A : 'G^n), replaceF i0 x0 A = 0 -> x0 = 0 /\ eqxF i0 A 0.
 Proof. move=>>; erewrite <- replaceF_zero at 1; apply replaceF_reg. Qed.
 
-Lemma replace2F_zero_reg_l :
-  forall {n} (A : 'G^n) x0 x1 i0 i1,
-    replace2F i0 i1 x0 x1 A = 0 -> eqx2F i0 i1 A 0.
-Proof. move=>>; erewrite <- replace2F_zero at 1; apply replace2F_reg_l. Qed.
-
-Lemma replace2F_zero_reg_r0 :
-  forall {n} (A : 'G^n) x0 x1 {i0 i1},
+Lemma replace2F_zero_reg_l0 :
+  forall {n} {i0 i1} x0 x1 (A : 'G^n),
     i1 <> i0 -> replace2F i0 i1 x0 x1 A = 0 -> x0 = 0.
-Proof. move=>>; erewrite <- replace2F_zero at 1; apply replace2F_reg_r0. Qed.
+Proof. move=>>; erewrite <- replace2F_zero at 1; apply replace2F_reg_l0. Qed.
 
-Lemma replace2F_zero_reg_r1 :
-  forall {n} (A : 'G^n) x0 x1 i0 i1, replace2F i0 i1 x0 x1 A = 0 -> x1 = 0.
-Proof. move=>>; erewrite <- replace2F_zero at 1; apply replace2F_reg_r1. Qed.
+Lemma replace2F_zero_reg_l1 :
+  forall {n} i0 i1 x0 x1 (A : 'G^n), replace2F i0 i1 x0 x1 A = 0 -> x1 = 0.
+Proof. move=>>; erewrite <- replace2F_zero at 1; apply replace2F_reg_l1. Qed.
+
+Lemma replace2F_zero_reg_r :
+  forall {n} i0 i1 x0 x1 (A : 'G^n),
+    replace2F i0 i1 x0 x1 A = 0 -> eqx2F i0 i1 A 0.
+Proof. move=>>; erewrite <- replace2F_zero at 1; apply replace2F_reg_r. Qed.
 
 Lemma replace2F_zero_reg :
-  forall {n} (A : 'G^n) x0 x1 {i0 i1},
+  forall {n} {i0 i1} x0 x1 (A : 'G^n),
     i1 <> i0 -> replace2F i0 i1 x0 x1 A = 0 ->
-    eqx2F i0 i1 A 0 /\ x0 = 0 /\ x1 = 0.
+    x0 = 0 /\ x1 = 0 /\ eqx2F i0 i1 A 0.
 Proof. move=>>; erewrite <- replace2F_zero at 1; apply replace2F_reg. Qed.
 
 Lemma mapF_zero_reg :
@@ -825,22 +825,22 @@ Lemma mapF_zero_reg_f :
 Proof. move=>> H; eapply mapF_inj_f; intros; apply H. Qed.
 
 Lemma eqxF_zero_equiv :
-  forall {n} (A : 'G^n.+1) i0, eqxF i0 A 0  <-> skipF i0 A = 0.
-Proof. intros n A i0; rewrite -(skipF_zero i0); apply eqxF_equiv. Qed.
+  forall {n} i0 (A : 'G^n.+1), eqxF i0 A 0  <-> skipF i0 A = 0.
+Proof. intros n i0 A; rewrite -(skipF_zero i0); apply eqxF_equiv. Qed.
 
 Lemma eqx2F_zero_equiv :
-  forall {n} (A : 'G^n.+2) {i0 i1} (H : i1 <> i0),
+  forall {n} {i0 i1} (H : i1 <> i0) (A : 'G^n.+2),
     eqx2F i0 i1 A 0 <-> skip2F H A = 0.
-Proof. intros n A i0 i1 H; rewrite -(skip2F_zero H); apply eqx2F_equiv. Qed.
+Proof. intros n i0 i1 H A; rewrite -(skip2F_zero H); apply eqx2F_equiv. Qed.
 
 Lemma neqxF_zero_equiv :
-  forall {n} (A : 'G^n.+1) i0, neqxF i0 A 0  <-> skipF i0 A <> 0.
-Proof. intros n A i0; rewrite -(skipF_zero i0); apply neqxF_equiv. Qed.
+  forall {n} i0 (A : 'G^n.+1), neqxF i0 A 0  <-> skipF i0 A <> 0.
+Proof. intros n i0 A; rewrite -(skipF_zero i0); apply neqxF_equiv. Qed.
 
 Lemma neqx2F_zero_equiv :
-  forall {n} (A : 'G^n.+2) {i0 i1} (H : i1 <> i0),
+  forall {n} {i0 i1} (H : i1 <> i0) (A : 'G^n.+2),
     neqx2F i0 i1 A 0 <-> skip2F H A <> 0.
-Proof. intros n A i0 i1 H; rewrite -(skip2F_zero H); apply neqx2F_equiv. Qed.
+Proof. intros n i0 i1 H A; rewrite -(skip2F_zero H); apply neqx2F_equiv. Qed.
 
 Lemma extF_zero_1 : forall {n} {A : 'G^n} i, n = 1 -> A i = 0 -> A = 0.
 Proof.
@@ -875,11 +875,11 @@ Lemma extF_zero_ind_r :
 Proof. intros; apply extF_ind_r; easy. Qed.
 
 Lemma extF_zero_skipF :
-  forall {n} (A : 'G^n.+1) i0, A i0 = 0 -> skipF i0 A = 0 -> A = 0.
-Proof. intros n A i0; rewrite -(skipF_zero i0); apply: extF_skipF. Qed.
+  forall {n} i0 (A : 'G^n.+1), A i0 = 0 -> skipF i0 A = 0 -> A = 0.
+Proof. intros n i0 A; rewrite -(skipF_zero i0); apply: extF_skipF. Qed.
 
 Lemma skipF_nextF_zero_reg :
-  forall {n} (A : 'G^n.+1) i0, skipF i0 A <> 0 -> neqxF i0 A 0 .
+  forall {n} i0 (A : 'G^n.+1), skipF i0 A <> 0 -> neqxF i0 A 0 .
 Proof. move=>>; erewrite <- skipF_zero; apply skipF_neqxF_reg. Qed.
 
 Lemma constF_zero_equiv : forall {n} (x : G), constF n.+1 x = 0 <-> x = 0.
@@ -936,7 +936,7 @@ intros; split; [apply concatF_zero_nextF_reg | intros [H | H]];
 Qed.
 
 Lemma insertF_zero_equiv :
-  forall {n} (A : 'G^n) x0 i0, insertF i0 x0 A = 0 <-> A = 0 /\ x0 = 0.
+  forall {n} i0 x0 (A : 'G^n), insertF i0 x0 A = 0 <-> x0 = 0 /\ A = 0.
 Proof.
 intros; split; [| intros; apply insertF_zero_compat; easy].
 intros H; split; move: H;
@@ -944,24 +944,24 @@ intros H; split; move: H;
 Qed.
 
 Lemma skipF_zero_equiv :
-  forall {n} (A : 'G^n.+1) i0, skipF i0 A = 0 <-> eqxF i0 A 0 .
+  forall {n} i0 (A : 'G^n.+1), skipF i0 A = 0 <-> eqxF i0 A 0 .
 Proof. intros; split; [apply skipF_zero_reg | apply skipF_zero_compat]. Qed.
 
 Lemma skip2F_zero_equiv :
-  forall {n} (A : 'G^n.+2) {i0 i1} (H : i1 <> i0),
+  forall {n} {i0 i1} (H : i1 <> i0) (A : 'G^n.+2),
     skip2F H A = 0 <-> eqx2F i0 i1 A 0.
 Proof. intros; split; [apply skip2F_zero_reg | apply skip2F_zero_compat]. Qed.
 
 Lemma replaceF_zero_equiv :
-  forall {n} (A : 'G^n) x0 i0, replaceF i0 x0 A = 0 <-> eqxF i0 A 0  /\ x0 = 0.
+  forall {n} i0 x0 (A : 'G^n), replaceF i0 x0 A = 0 <-> x0 = 0 /\ eqxF i0 A 0.
 Proof.
 intros; split; [apply replaceF_zero_reg |
     intros; apply replaceF_zero_compat; easy].
 Qed.
 
 Lemma replace2F_zero_equiv :
-  forall {n} (A : 'G^n) x0 x1 {i0 i1}, i1 <> i0 ->
-    replace2F i0 i1 x0 x1 A = 0 <-> eqx2F i0 i1 A 0 /\ x0 = 0 /\ x1 = 0.
+  forall {n} {i0 i1} x0 x1 (A : 'G^n), i1 <> i0 ->
+    replace2F i0 i1 x0 x1 A = 0 <-> x0 = 0 /\ x1 = 0 /\ eqx2F i0 i1 A 0.
 Proof.
 intros; split; [apply replace2F_zero_reg |
     intros; apply replace2F_zero_compat]; easy.
@@ -1031,22 +1031,22 @@ intros n1 n2 A1 B1 A2 B2; extF i; rewrite fct_plus_eq; destruct (lt_dec i n1);
 Qed.
 
 Lemma insertF_plus :
-  forall {n} (A B : 'G^n) a0 b0 i0,
+  forall {n} i0 a0 b0 (A B : 'G^n),
     insertF i0 (a0 + b0) (A + B) = insertF i0 a0 A + insertF i0 b0 B.
 Proof.
-intros n A B a0 b0 i0; extF i; rewrite fct_plus_eq; destruct (ord_eq_dec i i0);
+intros n i0 a0 b0 A B; extF i; rewrite fct_plus_eq; destruct (ord_eq_dec i i0);
     [rewrite !insertF_correct_l | rewrite !insertF_correct_r]; easy.
 Qed.
 
 Lemma skipF_plus :
-  forall {n} (A B : 'G^n.+1) i0, skipF i0 (A + B) = skipF i0 A + skipF i0 B.
+  forall {n} i0 (A B : 'G^n.+1), skipF i0 (A + B) = skipF i0 A + skipF i0 B.
 Proof. easy. Qed.
 
 Lemma replaceF_plus :
-  forall {n} (A B : 'G^n.+1) a0 b0 i0,
+  forall {n} i0 a0 b0 (A B : 'G^n.+1),
     replaceF i0 (a0 + b0) (A + B) = replaceF i0 a0 A + replaceF i0 b0 B.
 Proof.
-intros n A B a0 b0 i0; extF i; rewrite fct_plus_eq; destruct (ord_eq_dec i i0);
+intros n i0 a0 b0 A B; extF i; rewrite fct_plus_eq; destruct (ord_eq_dec i i0);
     [rewrite !replaceF_correct_l | rewrite !replaceF_correct_r]; easy.
 Qed.
 
diff --git a/Algebra/Monoid/Monoid_FT.v b/Algebra/Monoid/Monoid_FT.v
index 2f421b4e..876530f0 100644
--- a/Algebra/Monoid/Monoid_FT.v
+++ b/Algebra/Monoid/Monoid_FT.v
@@ -690,23 +690,23 @@ Lemma concatT_zero_reg :
 Proof. move=>>; rewrite -concatT_zero; apply concatT_inj. Qed.
 
 Lemma insertTr_zero_reg_l :
-  forall {m n} i0 A (M : 'G^{m,n}), insertTr i0 A M = 0 -> M = 0.
+  forall {m n} i0 A (M : 'G^{m,n}), insertTr i0 A M = 0 -> A = 0.
 Proof. move=>>; apply insertF_zero_reg_l. Qed.
 
 Lemma insertTr_zero_reg_r :
-  forall {m n} i0 A (M : 'G^{m,n}), insertTr i0 A M = 0 -> A = 0.
+  forall {m n} i0 A (M : 'G^{m,n}), insertTr i0 A M = 0 -> M = 0.
 Proof. move=>>; apply insertF_zero_reg_r. Qed.
 
 Lemma insertTc_zero_reg_l :
-  forall {m n} j0 B (M : 'G^{m,n}), insertTc j0 B M = 0 -> M = 0.
+  forall {m n} j0 B (M : 'G^{m,n}), insertTc j0 B M = 0 -> B = 0.
 Proof. move=>>; erewrite <- insertTc_zero at 1; apply insertTc_inj_l. Qed.
 
 Lemma insertTc_zero_reg_r :
-  forall {m n} j0 B (M : 'G^{m,n}), insertTc j0 B M = 0 -> B = 0.
+  forall {m n} j0 B (M : 'G^{m,n}), insertTc j0 B M = 0 -> M = 0.
 Proof. move=>>; erewrite <- insertTc_zero at 1; apply insertTc_inj_r. Qed.
 
 Lemma insertT_zero_reg_l :
-  forall {m n} i0 j0 x A B (M : 'G^{m,n}), insertT i0 j0 x A B M = 0 -> M = 0.
+  forall {m n} i0 j0 x A B (M : 'G^{m,n}), insertT i0 j0 x A B M = 0 -> x = 0.
 Proof. move=>>; erewrite <- insertT_zero at 1; apply insertT_inj_l. Qed.
 
 Lemma insertT_zero_reg_ml :
@@ -718,7 +718,7 @@ Lemma insertT_zero_reg_mr :
 Proof. move=>>; erewrite <- insertT_zero at 1; apply insertT_inj_mr. Qed.
 
 Lemma insertT_zero_reg_r :
-  forall {m n} i0 j0 x A B (M : 'G^{m,n}), insertT i0 j0 x A B M = 0 -> x = 0.
+  forall {m n} i0 j0 x A B (M : 'G^{m,n}), insertT i0 j0 x A B M = 0 -> M = 0.
 Proof. move=>>; erewrite <- insertT_zero at 1; apply insertT_inj_r. Qed.
 
 Lemma skipTr_zero_reg :
@@ -734,24 +734,23 @@ Lemma skipT_zero_reg :
 Proof. move=>>; erewrite <- skipT_zero; apply skipT_reg. Qed.
 
 Lemma replaceTr_zero_reg_l :
-  forall {m n} i0 A (M : 'G^{m,n}), replaceTr i0 A M = 0 -> eqxTr i0 M 0.
+  forall {m n} i0 A (M : 'G^{m,n}), replaceTr i0 A M = 0 -> A = 0.
 Proof. move=>>; apply replaceF_zero_reg_l. Qed.
 
 Lemma replaceTr_zero_reg_r :
-  forall {m n} i0 A (M : 'G^{m,n}), replaceTr i0 A M = 0 -> A = 0.
+  forall {m n} i0 A (M : 'G^{m,n}), replaceTr i0 A M = 0 -> eqxTr i0 M 0.
 Proof. move=>>; apply replaceF_zero_reg_r. Qed.
 
 Lemma replaceTc_zero_reg_l :
-  forall {m n} j0 B (M : 'G^{m,n}), replaceTc j0 B M = 0 -> eqxTc j0 M 0.
+  forall {m n} j0 B (M : 'G^{m,n}), replaceTc j0 B M = 0 -> B = 0.
 Proof. move=>>; erewrite <- replaceTc_zero at 1; apply replaceTc_reg_l. Qed.
 
 Lemma replaceTc_zero_reg_r :
-  forall {m n} j0 B (M : 'G^{m,n}), replaceTc j0 B M = 0 -> B = 0.
+  forall {m n} j0 B (M : 'G^{m,n}), replaceTc j0 B M = 0 -> eqxTc j0 M 0.
 Proof. move=>>; erewrite <- replaceTc_zero at 1; apply replaceTc_reg_r. Qed.
 
 Lemma replaceT_zero_reg_l :
-  forall {m n} i0 j0 x A B (M : 'G^{m,n}),
-    replaceT i0 j0 x A B M = 0 -> eqxT i0 j0 M 0.
+  forall {m n} i0 j0 x A B (M : 'G^{m,n}), replaceT i0 j0 x A B M = 0 -> x = 0.
 Proof. move=>>; erewrite <- replaceT_zero at 1; apply replaceT_reg_l. Qed.
 
 Lemma replaceT_zero_reg_ml :
@@ -765,7 +764,8 @@ Lemma replaceT_zero_reg_mr :
 Proof. move=>>; erewrite <- replaceT_zero at 1; apply replaceT_reg_mr. Qed.
 
 Lemma replaceT_zero_reg_r :
-  forall {m n} i0 j0 x A B (M : 'G^{m,n}), replaceT i0 j0 x A B M = 0 -> x = 0.
+  forall {m n} i0 j0 x A B (M : 'G^{m,n}),
+    replaceT i0 j0 x A B M = 0 -> eqxT i0 j0 M 0.
 Proof. move=>>; erewrite <- replaceT_zero at 1; apply replaceT_reg_r. Qed.
 
 Lemma mapT_zero_reg :
@@ -779,30 +779,30 @@ Lemma mapT_zero_reg_f :
 Proof. move=>> H; eapply mapT_inj_f; intros; apply H. Qed.
 
 Lemma eqxTr_zero_equiv :
-  forall {m n} (M : 'G^{m.+1,n}) i0, eqxTr i0 M 0 <-> skipTr i0 M = 0.
+  forall {m n} i0 (M : 'G^{m.+1,n}), eqxTr i0 M 0 <-> skipTr i0 M = 0.
 Proof. intros; apply eqxF_zero_equiv. Qed.
 
 Lemma eqxTc_zero_equiv :
-  forall {m n} (M : 'G^{m,n.+1}) j0, eqxTc j0 M 0 <-> skipTc j0 M = 0.
-Proof. intros m n M j0; rewrite -(skipTc_zero j0); apply eqxTc_equiv. Qed.
+  forall {m n} j0 (M : 'G^{m,n.+1}), eqxTc j0 M 0 <-> skipTc j0 M = 0.
+Proof. intros m n j0 M; rewrite -(skipTc_zero j0); apply eqxTc_equiv. Qed.
 
 Lemma eqxT_zero_equiv :
-  forall {m n} (M : 'G^{m.+1,n.+1}) i0 j0,
+  forall {m n} i0 j0 (M : 'G^{m.+1,n.+1}),
     eqxT i0 j0 M 0 <-> skipT i0 j0 M = 0.
-Proof. intros m n M i0 j0; rewrite -(skipT_zero i0 j0); apply eqxT_equiv. Qed.
+Proof. intros m n i0 j0 M; rewrite -(skipT_zero i0 j0); apply eqxT_equiv. Qed.
 
 Lemma neqxTr_zero_equiv :
-  forall {m n} (M : 'G^{m.+1,n}) i0, neqxTr i0 M 0 <-> skipTr i0 M <> 0.
+  forall {m n} i0 (M : 'G^{m.+1,n}), neqxTr i0 M 0 <-> skipTr i0 M <> 0.
 Proof. intros; apply neqxF_zero_equiv. Qed.
 
 Lemma neqxTc_zero_equiv :
-  forall {m n} (M : 'G^{m,n.+1}) j0, neqxTc j0 M 0 <-> skipTc j0 M <> 0.
-Proof. intros m n M j0; rewrite -(skipTc_zero j0); apply neqxTc_equiv. Qed.
+  forall {m n} j0 (M : 'G^{m,n.+1}), neqxTc j0 M 0 <-> skipTc j0 M <> 0.
+Proof. intros m n j0 M; rewrite -(skipTc_zero j0); apply neqxTc_equiv. Qed.
 
 Lemma neqxT_zero_equiv :
-  forall {m n} (M : 'G^{m.+1,n.+1}) i0 j0,
+  forall {m n} i0 j0 (M : 'G^{m.+1,n.+1}),
     neqxT i0 j0 M 0 <-> skipT i0 j0 M <> 0.
-Proof. intros m n M i0 j0; rewrite -(skipT_zero i0 j0); apply neqxT_equiv. Qed.
+Proof. intros m n i0 j0 M; rewrite -(skipT_zero i0 j0); apply neqxT_equiv. Qed.
 
 Lemma extTr_zero_splitTr :
   forall {m m1 m2 n} (Hm : m = (m1 + m2)%nat) (M : 'G^{m,n}),
@@ -826,28 +826,28 @@ apply Hul. apply Hur. apply Hdl. apply Hdr.
 Qed.
 
 Lemma extT_zero_skipTr :
-  forall {m n} (M : 'G^{m.+1,n}) i0, row M i0 = 0 -> skipTr i0 M = 0 -> M = 0.
+  forall {m n} i0 (M : 'G^{m.+1,n}), row M i0 = 0 -> skipTr i0 M = 0 -> M = 0.
 Proof. move=>>; apply extF_zero_skipF. Qed.
 
 Lemma extT_zero_skipTc :
-  forall {m n} (M : 'G^{m,n.+1}) j0, col M j0 = 0 -> skipTc j0 M = 0 -> M = 0.
+  forall {m n} j0 (M : 'G^{m,n.+1}), col M j0 = 0 -> skipTc j0 M = 0 -> M = 0.
 Proof. move=>>; erewrite <- skipTc_zero; apply: extT_skipTc. Qed.
 
 Lemma extT_zero_skipT :
-  forall {m n} (M : 'G^{m.+1,n.+1}) i0 j0,
+  forall {m n} i0 j0 (M : 'G^{m.+1,n.+1}),
     row M i0 = 0 -> col M j0 = 0 -> skipT i0 j0 M = 0 -> M = 0.
 Proof. move=>>; erewrite <- skipT_zero; apply: extT_skipT. Qed.
 
 Lemma skipTr_nextT_zero_reg :
-  forall {m n} (M : 'G^{m.+1,n}) i0, skipTr i0 M <> 0 -> neqxTr i0 M 0.
+  forall {m n} i0 (M : 'G^{m.+1,n}), skipTr i0 M <> 0 -> neqxTr i0 M 0.
 Proof. move=>>; apply skipF_nextF_zero_reg. Qed.
 
 Lemma skipTc_nextT_zero_reg :
-  forall {m n} (M : 'G^{m,n.+1}) j0, skipTc j0 M <> 0 -> neqxTc j0 M 0.
+  forall {m n} j0 (M : 'G^{m,n.+1}), skipTc j0 M <> 0 -> neqxTc j0 M 0.
 Proof. move=>>; erewrite <- skipTc_zero; apply skipTc_neqxTc_reg. Qed.
 
 Lemma skipT_nextT_zero_reg :
-  forall {m n} (M : 'G^{m.+1,n.+1}) i0 j0,
+  forall {m n} i0 j0 (M : 'G^{m.+1,n.+1}),
     skipT i0 j0 M <> 0 -> neqxT i0 j0 M 0.
 Proof. move=>>; erewrite <- skipT_zero; apply skipT_neqxT_reg. Qed.
 
diff --git a/Subsets/Finite_family.v b/Subsets/Finite_family.v
index e84b39f6..d1b1d9aa 100644
--- a/Subsets/Finite_family.v
+++ b/Subsets/Finite_family.v
@@ -2944,6 +2944,14 @@ Lemma insertF_eq :
 Proof. intros; f_equal; easy. Qed.
 
 Lemma insertF_inj_l :
+  forall {n} i0 x0 y0 (A B : 'E^n),
+    insertF i0 x0 A = insertF i0 y0 B -> x0 = y0.
+Proof.
+move=> n i0 x0 y0 A B /extF_rev H; specialize (H i0); simpl in H.
+rewrite -> 2!insertF_correct_l in H; easy.
+Qed.
+
+Lemma insertF_inj_r :
   forall {n} i0 x0 y0 (A B : 'E^n),
     insertF i0 x0 A = insertF i0 y0 B -> A = B.
 Proof.
@@ -2962,41 +2970,33 @@ apply lift_lt_r; easy.
 contradict Hi''; apply lift_m.
 Qed.
 
-Lemma insertF_inj_r :
-  forall {n} i0 x0 y0 (A B : 'E^n),
-    insertF i0 x0 A = insertF i0 y0 B -> x0 = y0.
-Proof.
-move=> n i0 x0 y0 A B /extF_rev H; specialize (H i0); simpl in H.
-rewrite -> 2!insertF_correct_l in H; easy.
-Qed.
-
 Lemma insertF_inj :
   forall {n} i0 x0 y0 (A B : 'E^n),
-    insertF i0 x0 A = insertF i0 y0 B -> A = B /\ x0 = y0.
+    insertF i0 x0 A = insertF i0 y0 B -> x0 = y0 /\ A = B.
 Proof.
 move=>> H; split; [eapply insertF_inj_l | eapply insertF_inj_r]; apply H.
 Qed.
 
 Lemma insertF_nextF_compat_l :
-  forall {n} i0 x0 y0 {A B : 'E^n},
-    A <> B -> insertF i0 x0 A <> insertF i0 y0 B.
+  forall {n} i0 {x0 y0} (A B : 'E^n),
+    x0 <> y0 -> insertF i0 x0 A <> insertF i0 y0 B.
 Proof. move=>> H; contradict H; apply insertF_inj in H; easy. Qed.
 
 Lemma insertF_nextF_compat_r :
-  forall {n} i0 {x0 y0} (A B : 'E^n),
-    x0 <> y0 -> insertF i0 x0 A <> insertF i0 y0 B.
+  forall {n} i0 x0 y0 {A B : 'E^n},
+    A <> B -> insertF i0 x0 A <> insertF i0 y0 B.
 Proof. move=>> H; contradict H; apply insertF_inj in H; easy. Qed.
 
 Lemma insertF_nextF_reg :
   forall {n} i0 {x0 y0} {A B : 'E^n},
-    insertF i0 x0 A <> insertF i0 y0 B -> A <> B \/ x0 <> y0.
+    insertF i0 x0 A <> insertF i0 y0 B -> x0 <> y0 \/ A <> B.
 Proof.
 move=>> H; apply not_and_or; contradict H; apply insertF_eq; easy.
 Qed.
 
 Lemma insertF_nextF_equiv :
   forall {n} i0 {x0 y0} {A B : 'E^n},
-    insertF i0 x0 A <> insertF i0 y0 B <-> A <> B \/ x0 <> y0.
+    insertF i0 x0 A <> insertF i0 y0 B <-> x0 <> y0 \/ A <> B.
 Proof.
 intros; split; [apply insertF_nextF_reg | intros [H | H]];
     [apply insertF_nextF_compat_l | apply insertF_nextF_compat_r]; easy.
@@ -3203,67 +3203,67 @@ Lemma insert2F_eq :
     x0 = y0 -> x1 = y1 -> A = B -> insert2F H x0 x1 A = insert2F H y0 y1 B.
 Proof. intros; apply insert2F_eq_gen; easy. Qed.
 
-Lemma insert2F_inj_l :
+Lemma insert2F_inj_l0 :
   forall {n i0 i1} (H : i1 <> i0) x0 x1 y0 y1 (A B : 'E^n),
-    insert2F H x0 x1 A = insert2F H y0 y1 B -> A = B.
+    insert2F H x0 x1 A = insert2F H y0 y1 B -> x0 = y0.
 Proof.
-move=>> H; rewrite 2!insert2F_correct in H; apply insertF_inj_l in H.
-eapply insertF_inj_l, H.
+move=>> H; rewrite 2!insert2F_correct in H; eapply insertF_inj_l, H.
 Qed.
 
-Lemma insert2F_inj_r0 :
+Lemma insert2F_inj_l1 :
   forall {n i0 i1} (H : i1 <> i0) x0 x1 y0 y1 (A B : 'E^n),
-    insert2F H x0 x1 A = insert2F H y0 y1 B -> x0 = y0.
+    insert2F H x0 x1 A = insert2F H y0 y1 B -> x1 = y1.
 Proof.
-move=>> H; rewrite 2!insert2F_correct in H; eapply insertF_inj_r, H.
+move=>> H; rewrite 2!insert2F_correct in H; apply insertF_inj_r in H.
+eapply insertF_inj_l, H.
 Qed.
 
-Lemma insert2F_inj_r1 :
+Lemma insert2F_inj_r :
   forall {n i0 i1} (H : i1 <> i0) x0 x1 y0 y1 (A B : 'E^n),
-    insert2F H x0 x1 A = insert2F H y0 y1 B -> x1 = y1.
+    insert2F H x0 x1 A = insert2F H y0 y1 B -> A = B.
 Proof.
-move=>> H; rewrite 2!insert2F_correct in H; apply insertF_inj_l in H.
+move=>> H; rewrite 2!insert2F_correct in H; apply insertF_inj_r in H.
 eapply insertF_inj_r, H.
 Qed.
 
 Lemma insert2F_inj :
   forall {n i0 i1} (H : i1 <> i0) x0 x1 y0 y1 (A B : 'E^n),
-    insert2F H x0 x1 A = insert2F H y0 y1 B -> A = B /\ x0 = y0 /\ x1 = y1.
+    insert2F H x0 x1 A = insert2F H y0 y1 B -> x0 = y0 /\ x1 = y1 /\ A = B.
 Proof.
 move=>> H; repeat split;
-    [eapply insert2F_inj_l | eapply insert2F_inj_r0 | eapply insert2F_inj_r1];
+    [eapply insert2F_inj_l0 | eapply insert2F_inj_l1 | eapply insert2F_inj_r];
     apply H.
 Qed.
 
-Lemma insert2F_nextF_compat_l :
-  forall {n i0 i1} (H : i1 <> i0) x0 x1 y0 y1 {A B : 'E^n},
-    A <> B -> insert2F H x0 x1 A <> insert2F H y0 y1 B.
-Proof. move=>> H; contradict H; apply insert2F_inj in H; easy. Qed.
-
-Lemma insert2F_nextF_compat_r0 :
+Lemma insert2F_nextF_compat_l0 :
   forall {n i0 i1} (H : i1 <> i0) {x0} x1 {y0} y1 (A B : 'E^n),
     x0 <> y0 -> insert2F H x0 x1 A <> insert2F H y0 y1 B.
-Proof. move=>> H; contradict H; apply insert2F_inj_r0 in H; easy. Qed.
+Proof. move=>> H; contradict H; apply insert2F_inj_l0 in H; easy. Qed.
 
-Lemma insert2F_nextF_compat_r1 :
+Lemma insert2F_nextF_compat_l1 :
   forall {n i0 i1} (H : i1 <> i0) x0 {x1} y0 {y1} (A B : 'E^n),
     x1 <> y1 -> insert2F H x0 x1 A <> insert2F H y0 y1 B.
-Proof. move=>> H; contradict H; apply insert2F_inj_r1 in H; easy. Qed.
+Proof. move=>> H; contradict H; apply insert2F_inj_l1 in H; easy. Qed.
+
+Lemma insert2F_nextF_compat_r :
+  forall {n i0 i1} (H : i1 <> i0) x0 x1 y0 y1 {A B : 'E^n},
+    A <> B -> insert2F H x0 x1 A <> insert2F H y0 y1 B.
+Proof. move=>> H; contradict H; apply insert2F_inj in H; easy. Qed.
 
 Lemma insert2F_nextF_reg :
   forall {n i0 i1} (H : i1 <> i0) {x0 x1 y0 y1} {A B : 'E^n},
-    insert2F H x0 x1 A <> insert2F H y0 y1 B -> A <> B \/ x0 <> y0 \/ x1 <> y1.
+    insert2F H x0 x1 A <> insert2F H y0 y1 B -> x0 <> y0 \/ x1 <> y1 \/ A <> B.
 Proof.
 move=>> H; apply not_and3_equiv; contradict H; apply insert2F_eq; easy.
 Qed.
 
 Lemma insert2F_nextF_equiv :
   forall {n i0 i1} (H : i1 <> i0) {x0 x1 y0 y1} {A B : 'E^n},
-    insert2F H x0 x1 A <> insert2F H y0 y1 B <-> A <> B \/ x0 <> y0 \/ x1 <> y1.
+    insert2F H x0 x1 A <> insert2F H y0 y1 B <-> x0 <> y0 \/ x1 <> y1 \/ A <> B.
 Proof.
 intros; split; [apply insert2F_nextF_reg | intros [H1 | [H1 | H1]]];
-    [apply insert2F_nextF_compat_l |
-     apply insert2F_nextF_compat_r0 | apply insert2F_nextF_compat_r1]; easy.
+    [apply insert2F_nextF_compat_l0 | apply insert2F_nextF_compat_l1 |
+    apply insert2F_nextF_compat_r]; easy.
 Qed.
 
 Lemma insert2F_singleF_01 :
@@ -3898,14 +3898,6 @@ Lemma replaceF_eq :
 Proof. intros; apply replaceF_eq_gen; easy. Qed.
 
 Lemma replaceF_reg_l :
-  forall {n i0 x0 y0} {A B : 'E^n},
-    replaceF i0 x0 A = replaceF i0 y0 B -> eqxF i0 A B.
-Proof.
-move=>> /extF_rev H i Hi; specialize (H i); simpl in H.
-erewrite 2!replaceF_correct_r in H; easy.
-Qed.
-
-Lemma replaceF_reg_r :
   forall {n i0 x0 y0} (A B : 'E^n),
     replaceF i0 x0 A = replaceF i0 y0 B -> x0 = y0.
 Proof.
@@ -3913,9 +3905,17 @@ move=> n i0 x0 y0 A B /extF_rev H; specialize (H i0); simpl in H.
 erewrite 2!replaceF_correct_l in H; easy.
 Qed.
 
+Lemma replaceF_reg_r :
+  forall {n i0 x0 y0} {A B : 'E^n},
+    replaceF i0 x0 A = replaceF i0 y0 B -> eqxF i0 A B.
+Proof.
+move=>> /extF_rev H i Hi; specialize (H i); simpl in H.
+erewrite 2!replaceF_correct_r in H; easy.
+Qed.
+
 Lemma replaceF_reg :
   forall {n i0 x0 y0} {A B : 'E^n},
-    replaceF i0 x0 A = replaceF i0 y0 B -> eqxF i0 A B /\ x0 = y0.
+    replaceF i0 x0 A = replaceF i0 y0 B -> x0 = y0 /\ eqxF i0 A B.
 Proof.
 move=>> H; split; [eapply replaceF_reg_l | eapply replaceF_reg_r]; apply H.
 Qed.
@@ -3932,18 +3932,18 @@ rewrite -> 2!replaceF_correct_r; auto.
 Qed.
 
 Lemma replaceF_neqxF_compat_l :
-  forall {n i0} x0 y0 {A B : 'E^n},
-    neqxF i0 A B -> replaceF i0 x0 A <> replaceF i0 y0 B.
-Proof. move=>>; rewrite neqxF_not_equiv -contra_equiv; apply replaceF_reg. Qed.
-
-Lemma replaceF_neqxF_compat_r :
   forall {n} i0 {x0 y0} {A B : 'E^n},
     x0 <> y0 -> replaceF i0 x0 A <> replaceF i0 y0 B.
 Proof. move=>>; rewrite -contra_equiv; apply replaceF_reg. Qed.
 
+Lemma replaceF_neqxF_compat_r :
+  forall {n i0} x0 y0 {A B : 'E^n},
+    neqxF i0 A B -> replaceF i0 x0 A <> replaceF i0 y0 B.
+Proof. move=>>; rewrite neqxF_not_equiv -contra_equiv; apply replaceF_reg. Qed.
+
 Lemma replaceF_neqxF_reg :
   forall {n i0 x0 y0} {A B : 'E^n},
-    replaceF i0 x0 A <> replaceF i0 y0 B -> neqxF i0 A B \/ x0 <> y0.
+    replaceF i0 x0 A <> replaceF i0 y0 B -> x0 <> y0 \/ neqxF i0 A B.
 Proof.
 move=>>; rewrite neqxF_not_equiv -not_and_equiv -contra_equiv.
 intros; apply replaceF_eq; easy.
@@ -3951,7 +3951,7 @@ Qed.
 
 Lemma replaceF_neqxF_equiv :
   forall {n i0 x0 y0} {A B : 'E^n},
-    replaceF i0 x0 A <> replaceF i0 y0 B <-> neqxF i0 A B \/ x0 <> y0.
+    replaceF i0 x0 A <> replaceF i0 y0 B <-> x0 <> y0 \/ neqxF i0 A B.
 Proof.
 intros; split; [apply replaceF_neqxF_reg | intros [H | H]];
     [apply replaceF_neqxF_compat_l | apply replaceF_neqxF_compat_r]; easy.
@@ -3960,7 +3960,7 @@ Qed.
 Lemma neqxF_replaceF :
   forall {n} i0 i1 x1 y1 (A B : 'E^n),
     neqxF i0 (replaceF i1 x1 A) (replaceF i1 y1 B) ->
-    neqx2F i0 i1 A B \/ x1 <> y1.
+    x1 <> y1 \/ neqx2F i0 i1 A B.
 Proof.
 move=>>; rewrite neqxF_not_equiv neqx2F_not_equiv -not_and_equiv -contra_equiv.
 intros; apply eqxF_replaceF; easy.
@@ -4062,57 +4062,57 @@ Lemma replace2F_eq :
     replace2F i0 i1 x0 x1 A = replace2F i0 i1 y0 y1 B.
 Proof. intros; apply replace2F_eq_gen; easy. Qed.
 
-Lemma replace2F_reg_l :
-  forall {n} i0 i1 x0 x1 y0 y1 (A B : 'E^n),
-    replace2F i0 i1 x0 x1 A = replace2F i0 i1 y0 y1 B -> eqx2F i0 i1 A B.
-Proof.
-move=>> H2 i [Hi0 Hi1]; unfold replace2F in H2.
-specialize (replaceF_reg_l H2 i Hi1); intros H1.
-erewrite 2!replaceF_correct_r in H1; easy.
-Qed.
-
-Lemma replace2F_reg_r0 :
+Lemma replace2F_reg_l0 :
   forall {n i0 i1} x0 x1 y0 y1 (A B : 'E^n),
     i1 <> i0 -> replace2F i0 i1 x0 x1 A = replace2F i0 i1 y0 y1 B -> x0 = y0.
 Proof.
-move=>> H; rewrite -> 2!replace2F_equiv_def; try easy; apply replaceF_reg_r.
+move=>> H; rewrite -> 2!replace2F_equiv_def; try easy; apply replaceF_reg_l.
 Qed.
 
-Lemma replace2F_reg_r1 :
+Lemma replace2F_reg_l1 :
   forall {n} i0 i1 x0 x1 y0 y1 (A B : 'E^n),
     replace2F i0 i1 x0 x1 A = replace2F i0 i1 y0 y1 B -> x1 = y1.
-Proof. move=>>; apply replaceF_reg_r. Qed.
+Proof. move=>>; apply replaceF_reg_l. Qed.
 
-Lemma replace2F_reg :
-  forall {n i0 i1} x0 x1 y0 y1 (A B : 'E^n),
-    i1 <> i0 -> replace2F i0 i1 x0 x1 A = replace2F i0 i1 y0 y1 B ->
-    eqx2F i0 i1 A B /\ x0 = y0 /\ x1 = y1.
+Lemma replace2F_reg_r :
+  forall {n} i0 i1 x0 x1 y0 y1 (A B : 'E^n),
+    replace2F i0 i1 x0 x1 A = replace2F i0 i1 y0 y1 B -> eqx2F i0 i1 A B.
 Proof.
-move=>> Hi; repeat split; [eapply replace2F_reg_l |
-    eapply replace2F_reg_r0 | eapply replace2F_reg_r1]; try apply H; easy.
+move=>> H2 i [Hi0 Hi1]; unfold replace2F in H2.
+specialize (replaceF_reg_r H2 i Hi1); intros H1.
+erewrite 2!replaceF_correct_r in H1; easy.
 Qed.
 
-Lemma replace2F_neqxF_compat_l :
-  forall {n i0 i1} x0 x1 y0 y1 {A B : 'E^n},
-    neqx2F i0 i1 A B -> replace2F i0 i1 x0 x1 A <> replace2F i0 i1 y0 y1 B.
+Lemma replace2F_reg :
+  forall {n i0 i1} x0 x1 y0 y1 (A B : 'E^n),
+    i1 <> i0 -> replace2F i0 i1 x0 x1 A = replace2F i0 i1 y0 y1 B ->
+    x0 = y0 /\ x1 = y1 /\ eqx2F i0 i1 A B.
 Proof.
-move=>>; rewrite neqx2F_not_equiv -contra_equiv; apply replace2F_reg_l.
+move=>> Hi; repeat split; [eapply replace2F_reg_l0 |
+    eapply replace2F_reg_l1 | eapply replace2F_reg_r]; try apply H; easy.
 Qed.
 
-Lemma replace2F_neqxF_compat_r0 :
+Lemma replace2F_neqxF_compat_l0 :
   forall {n i0 i1 x0} x1 {y0} y1 (A B : 'E^n),
     i1 <> i0 -> x0 <> y0 -> replace2F i0 i1 x0 x1 A <> replace2F i0 i1 y0 y1 B.
-Proof. move=>>; rewrite -contra_equiv; apply replace2F_reg_r0. Qed.
+Proof. move=>>; rewrite -contra_equiv; apply replace2F_reg_l0. Qed.
 
-Lemma replace2F_neqxF_compat_r1 :
+Lemma replace2F_neqxF_compat_l1 :
   forall {n} i0 i1 x0 {x1} y0 {y1} (A B : 'E^n),
     x1 <> y1 -> replace2F i0 i1 x0 x1 A <> replace2F i0 i1 y0 y1 B.
-Proof. move=>>; rewrite -contra_equiv; apply replace2F_reg_r1. Qed.
+Proof. move=>>; rewrite -contra_equiv; apply replace2F_reg_l1. Qed.
+
+Lemma replace2F_neqxF_compat_r :
+  forall {n i0 i1} x0 x1 y0 y1 {A B : 'E^n},
+    neqx2F i0 i1 A B -> replace2F i0 i1 x0 x1 A <> replace2F i0 i1 y0 y1 B.
+Proof.
+move=>>; rewrite neqx2F_not_equiv -contra_equiv; apply replace2F_reg_r.
+Qed.
 
 Lemma replace2F_neqxF_reg :
   forall {n x0 x1 y0 y1 i0 i1} {A B : 'E^n},
     replace2F i0 i1 x0 x1 A <> replace2F i0 i1 y0 y1 B ->
-    neqx2F i0 i1 A B \/ x0 <> y0 \/ x1 <> y1.
+    x0 <> y0 \/ x1 <> y1 \/ neqx2F i0 i1 A B.
 Proof.
 move=>>; rewrite neqx2F_not_equiv -not_and3_equiv -contra_equiv.
 intros; apply replace2F_eq; easy.
@@ -4121,11 +4121,11 @@ Qed.
 Lemma replace2F_neqxF_equiv :
   forall {n i0 i1 x0 x1 y0 y1} {A B : 'E^n},
     i1 <> i0 -> replace2F i0 i1 x0 x1 A <> replace2F i0 i1 y0 y1 B <->
-    neqx2F i0 i1 A B \/ x0 <> y0 \/ x1 <> y1.
+    x0 <> y0 \/ x1 <> y1 \/ neqx2F i0 i1 A B.
 Proof.
 intros; split; [apply replace2F_neqxF_reg | intros [H1 | [H1 | H1]]];
-    [apply replace2F_neqxF_compat_l |
-     apply replace2F_neqxF_compat_r0 | apply replace2F_neqxF_compat_r1]; easy.
+    [apply replace2F_neqxF_compat_l0 | apply replace2F_neqxF_compat_l1 |
+    apply replace2F_neqxF_compat_r]; easy.
 Qed.
 
 Lemma replace2F_constF :
diff --git a/Subsets/Finite_table.v b/Subsets/Finite_table.v
index 5d636bfc..ac886456 100644
--- a/Subsets/Finite_table.v
+++ b/Subsets/Finite_table.v
@@ -2176,60 +2176,60 @@ Proof. intros; f_equal; easy. Qed.
 
 Lemma insertTr_inj_l :
   forall {m n} i0 A C (M N : 'E^{m,n}),
-    insertTr i0 A M = insertTr i0 C N -> M = N.
+    insertTr i0 A M = insertTr i0 C N -> A = C.
 Proof. move=>> H; eapply insertF_inj_l; apply H. Qed.
 
 Lemma insertTr_inj_r :
   forall {m n} i0 A C (M N : 'E^{m,n}),
-    insertTr i0 A M = insertTr i0 C N -> A = C.
+    insertTr i0 A M = insertTr i0 C N -> M = N.
 Proof. move=>> H; eapply insertF_inj_r; apply H. Qed.
 
 Lemma insertTr_inj :
   forall {m n} i0 A C (M N : 'E^{m,n}),
-    insertTr i0 A M = insertTr i0 C N -> M = N /\ A = C.
+    insertTr i0 A M = insertTr i0 C N -> A = C /\ M = N.
 Proof. move=>> H; eapply insertF_inj; apply H. Qed.
 
-Lemma insertTc_inj_l :
+Lemma insertTc_inj_r :
   forall {m n} j0 B D (M N : 'E^{m,n}),
     insertTc j0 B M = insertTc j0 D N -> M = N.
-Proof. move=>> /extF_rev H; extF; eapply insertF_inj_l; apply H. Qed.
+Proof. move=>> /extF_rev H; extF; eapply insertF_inj_r; apply H. Qed.
 
-Lemma insertTc_inj_r :
+Lemma insertTc_inj_l :
   forall {m n} j0 B D (M N : 'E^{m,n}),
     insertTc j0 B M = insertTc j0 D N -> B = D.
-Proof. move=>> /extF_rev H; extF; eapply insertF_inj_r; apply H. Qed.
+Proof. move=>> /extF_rev H; extF; eapply insertF_inj_l; apply H. Qed.
 
 Lemma insertTc_inj :
   forall {m n} j0 B D (M N : 'E^{m,n}),
-    insertTc j0 B M = insertTc j0 D N -> M = N /\ B = D.
+    insertTc j0 B M = insertTc j0 D N -> B = D /\ M = N.
 Proof.
 move=>> H; split; [eapply insertTc_inj_l | eapply insertTc_inj_r]; apply H.
 Qed.
 
 Lemma insertT_inj_l :
   forall {m n} i0 j0 x y A C B D (M N : 'E^{m,n}),
-    insertT i0 j0 x A B M = insertT i0 j0 y C D N -> M = N.
-Proof. move=>> H; eapply insertTc_inj_l, insertTr_inj_l; apply H. Qed.
+    insertT i0 j0 x A B M = insertT i0 j0 y C D N -> x = y.
+Proof. move=>> /insertTr_inj_l H; eapply insertF_inj_l; apply H. Qed.
 
 Lemma insertT_inj_ml :
   forall {m n} i0 j0 x y A C B D (M N : 'E^{m,n}),
     insertT i0 j0 x A B M = insertT i0 j0 y C D N -> A = C.
-Proof. move=>> /insertTr_inj_r H; eapply insertF_inj_l; apply H. Qed.
+Proof. move=>> /insertTr_inj_l H; eapply insertF_inj_r; apply H. Qed.
 
 Lemma insertT_inj_mr :
   forall {m n} i0 j0 x y A C B D (M N : 'E^{m,n}),
     insertT i0 j0 x A B M = insertT i0 j0 y C D N -> B = D.
-Proof. move=>> /insertTr_inj_l H; eapply insertTc_inj_r; apply H. Qed.
+Proof. move=>> /insertTr_inj_r H; eapply insertTc_inj_l; apply H. Qed.
 
 Lemma insertT_inj_r :
   forall {m n} i0 j0 x y A C B D (M N : 'E^{m,n}),
-    insertT i0 j0 x A B M = insertT i0 j0 y C D N -> x = y.
-Proof. move=>> /insertTr_inj_r H; eapply insertF_inj_r; apply H. Qed.
+    insertT i0 j0 x A B M = insertT i0 j0 y C D N -> M = N.
+Proof. move=>> H; eapply insertTc_inj_r, insertTr_inj_r; apply H. Qed.
 
 Lemma insertT_inj :
   forall {m n} i0 j0 x y A C B D (M N : 'E^{m,n}),
     insertT i0 j0 x A B M = insertT i0 j0 y C D N ->
-    M = N /\ A = C /\ B = D /\ x = y.
+    x = y /\ A = C /\ B = D /\ M = N.
 Proof.
 move=>> H; repeat split;
     [eapply insertT_inj_l | eapply insertT_inj_ml |
@@ -2237,41 +2237,41 @@ move=>> H; repeat split;
 Qed.
 
 Lemma insertTr_nextT_compat_l :
-  forall {m n} i0 A C {M N : 'E^{m,n}},
-    M <> N -> insertTr i0 A M <> insertTr i0 C N.
+  forall {m n} i0 {A C} (M N : 'E^{m,n}),
+    A <> C -> insertTr i0 A M <> insertTr i0 C N.
 Proof. move=>>; apply insertF_nextF_compat_l. Qed.
 
 Lemma insertTr_nextT_compat_r :
-  forall {m n} i0 {A C} (M N : 'E^{m,n}),
-    A <> C -> insertTr i0 A M <> insertTr i0 C N.
+  forall {m n} i0 A C {M N : 'E^{m,n}},
+    M <> N -> insertTr i0 A M <> insertTr i0 C N.
 Proof. move=>>; apply insertF_nextF_compat_r. Qed.
 
 Lemma insertTr_nextT_reg :
   forall {m n} i0 {A C} {M N : 'E^{m,n}},
-    insertTr i0 A M <> insertTr i0 C N -> M <> N \/ A <> C.
+    insertTr i0 A M <> insertTr i0 C N -> A <> C \/ M <> N.
 Proof. move=>>; apply insertF_nextF_reg. Qed.
 
 Lemma insertTr_nextT_equiv :
   forall {m n} i0 {A C} {M N : 'E^{m,n}},
-    insertTr i0 A M <> insertTr i0 C N <-> M <> N \/ A <> C.
+    insertTr i0 A M <> insertTr i0 C N <-> A <> C \/ M <> N.
 Proof.
 intros; split; [apply insertTr_nextT_reg | intros [H | H]];
     [apply insertTr_nextT_compat_l | apply insertTr_nextT_compat_r]; easy.
 Qed.
 
 Lemma insertTc_nextT_compat_l :
-  forall {m n} j0 B D {M N : 'E^{m,n}},
-    M <> N -> insertTc j0 B M <> insertTc j0 D N.
+  forall {m n} j0 {B D} (M N : 'E^{m,n}),
+    B <> D -> insertTc j0 B M <> insertTc j0 D N.
 Proof. move=>> H; contradict H; apply insertTc_inj in H; easy. Qed.
 
 Lemma insertTc_nextT_compat_r :
-  forall {m n} j0 {B D} (M N : 'E^{m,n}),
-    B <> D -> insertTc j0 B M <> insertTc j0 D N.
+  forall {m n} j0 B D {M N : 'E^{m,n}},
+    M <> N -> insertTc j0 B M <> insertTc j0 D N.
 Proof. move=>> H; contradict H; apply insertTc_inj in H; easy. Qed.
 
 Lemma insertTc_nextT_reg :
   forall {m n} j0 {B D} {M N : 'E^{m,n}},
-    insertTc j0 B M <> insertTc j0 D N -> M <> N \/ B <> D.
+    insertTc j0 B M <> insertTc j0 D N -> B <> D \/ M <> N.
 Proof.
 move=>>; rewrite -not_and_equiv -contra_equiv.
 intros; apply insertTc_eq; easy.
@@ -2279,15 +2279,15 @@ Qed.
 
 Lemma insertTc_nextT_equiv :
   forall {m n} j0 {B D} {M N : 'E^{m,n}},
-    insertTc j0 B M <> insertTc j0 D N <-> M <> N \/ B <> D.
+    insertTc j0 B M <> insertTc j0 D N <-> B <> D \/ M <> N.
 Proof.
 intros; split; [apply insertTc_nextT_reg | intros [H | H]];
     [apply insertTc_nextT_compat_l | apply insertTc_nextT_compat_r]; easy.
 Qed.
 
 Lemma insertT_nextT_compat_l :
-  forall {m n} i0 j0 x y A C B D {M N : 'E^{m,n}},
-    M <> N -> insertT i0 j0 x A B M <> insertT i0 j0 y C D N.
+  forall {m n} i0 j0 {x y} A C B D (M N : 'E^{m,n}),
+    x <> y -> insertT i0 j0 x A B M <> insertT i0 j0 y C D N.
 Proof. move=>> H; contradict H; apply insertT_inj in H; easy. Qed.
 
 Lemma insertT_nextT_compat_ml :
@@ -2301,14 +2301,14 @@ Lemma insertT_nextT_compat_mr :
 Proof. move=>> H; contradict H; apply insertT_inj in H; easy. Qed.
 
 Lemma insertT_nextT_compat_r :
-  forall {m n} i0 j0 {x y} A C B D (M N : 'E^{m,n}),
-    x <> y -> insertT i0 j0 x A B M <> insertT i0 j0 y C D N.
+  forall {m n} i0 j0 x y A C B D {M N : 'E^{m,n}},
+    M <> N -> insertT i0 j0 x A B M <> insertT i0 j0 y C D N.
 Proof. move=>> H; contradict H; apply insertT_inj in H; easy. Qed.
 
 Lemma insertT_nextT_reg :
   forall {m n} i0 j0 {x y A C B D} {M N : 'E^{m,n}},
     insertT i0 j0 x A B M <> insertT i0 j0 y C D N ->
-    M <> N \/ A <> C \/ B <> D \/ x <> y.
+    x <> y \/ A <> C \/ B <> D \/ M <> N.
 Proof.
 move=>>; rewrite -not_and4_equiv -contra_equiv.
 intros; apply insertT_eq; easy.
@@ -2317,7 +2317,7 @@ Qed.
 Lemma insertT_nextT_equiv :
   forall {m n} i0 j0 {x y A C B D} {M N : 'E^{m,n}},
     insertT i0 j0 x A B M <> insertT i0 j0 y C D N <->
-    M <> N \/ A <> C \/ B <> D \/ x <> y.
+    x <> y \/ A <> C \/ B <> D \/ M <> N.
 Proof.
 intros; split; [apply insertT_nextT_reg | intros [H | [H | [H | H]]]];
     [apply insertT_nextT_compat_l | apply insertT_nextT_compat_ml |
@@ -2837,71 +2837,71 @@ Proof. intros; apply replaceT_eq_gen; easy. Qed.
 
 Lemma replaceTr_reg_l :
   forall {m n} i0 A C (M N : 'E^{m,n}),
-    replaceTr i0 A M = replaceTr i0 C N -> eqxTr i0 M N.
+    replaceTr i0 A M = replaceTr i0 C N -> A = C.
 Proof. move=>> H; eapply replaceF_reg_l; apply H. Qed.
 
 Lemma replaceTr_reg_r :
   forall {m n} i0 A C (M N : 'E^{m,n}),
-    replaceTr i0 A M = replaceTr i0 C N -> A = C.
+    replaceTr i0 A M = replaceTr i0 C N -> eqxTr i0 M N.
 Proof. move=>> H; eapply replaceF_reg_r; apply H. Qed.
 
 Lemma replaceTr_reg :
   forall {m n} i0 A C (M N : 'E^{m,n}),
-    replaceTr i0 A M = replaceTr i0 C N -> eqxTr i0 M N /\ A = C.
+    replaceTr i0 A M = replaceTr i0 C N -> A = C /\ eqxTr i0 M N.
 Proof. move=>> H; eapply replaceF_reg; apply H. Qed.
 
 Lemma replaceTc_reg_l :
   forall {m n} j0 B D (M N : 'E^{m,n}),
-    replaceTc j0 B M = replaceTc j0 D N -> eqxTc j0 M N.
+    replaceTc j0 B M = replaceTc j0 D N -> B = D.
 Proof.
-move=>> /flipT_eq; rewrite 2!flipT_replaceTc.
-move=> /replaceTr_reg_l; apply eqxTr_flipT.
+move=>> /flipT_eq; rewrite 2!flipT_replaceTc; apply replaceTr_reg_l.
 Qed.
 
 Lemma replaceTc_reg_r :
   forall {m n} j0 B D (M N : 'E^{m,n}),
-    replaceTc j0 B M = replaceTc j0 D N -> B = D.
+    replaceTc j0 B M = replaceTc j0 D N -> eqxTc j0 M N.
 Proof.
-move=>> /flipT_eq; rewrite 2!flipT_replaceTc; apply replaceTr_reg_r.
+move=>> /flipT_eq; rewrite 2!flipT_replaceTc.
+move=> /replaceTr_reg_r; apply eqxTr_flipT.
 Qed.
 
 Lemma replaceTc_reg :
   forall {m n} j0 B D (M N : 'E^{m,n}),
-    replaceTc j0 B M = replaceTc j0 D N -> eqxTc j0 M N /\ B = D.
+    replaceTc j0 B M = replaceTc j0 D N -> B = D /\ eqxTc j0 M N.
 Proof.
 move=>> H; split; [eapply replaceTc_reg_l | eapply replaceTc_reg_r]; apply H.
 Qed.
 
 Lemma replaceT_reg_l :
   forall {m n} i0 j0 x y A C B D (M N : 'E^{m,n}),
-    replaceT i0 j0 x A B M = replaceT i0 j0 y C D N -> eqxT i0 j0 M N.
-Proof.
-move=>> /extT_rev H i j Hi Hj; specialize (H i j); simpl in H.
-erewrite 2!replaceT_correct_r in H; easy.
-Qed.
+    replaceT i0 j0 x A B M = replaceT i0 j0 y C D N -> x = y.
+Proof. move=>> /replaceTr_reg_l H; eapply replaceF_reg_l; apply H. Qed.
 
 Lemma replaceT_reg_ml :
   forall {m n} i0 j0 x y A C B D (M N : 'E^{m,n}),
     replaceT i0 j0 x A B M = replaceT i0 j0 y C D N -> eqxF j0 A C.
-Proof. move=>> /replaceTr_reg_r H; eapply replaceF_reg_l; apply H. Qed.
+Proof. move=>> /replaceTr_reg_l H; eapply replaceF_reg_r; apply H. Qed.
 
 Lemma replaceT_reg_mr :
   forall {m n} i0 j0 x y A C B D (M N : 'E^{m,n}),
     replaceT i0 j0 x A B M = replaceT i0 j0 y C D N -> eqxF i0 B D.
 Proof.
 move=>>; rewrite 2!replaceT_equiv_def.
-move=> /replaceTc_reg_r H; eapply replaceF_reg_l; apply H.
+move=> /replaceTc_reg_l H; eapply replaceF_reg_r; apply H.
 Qed.
 
 Lemma replaceT_reg_r :
   forall {m n} i0 j0 x y A C B D (M N : 'E^{m,n}),
-    replaceT i0 j0 x A B M = replaceT i0 j0 y C D N -> x = y.
-Proof. move=>> /replaceTr_reg_r H; eapply replaceF_reg_r; apply H. Qed.
+    replaceT i0 j0 x A B M = replaceT i0 j0 y C D N -> eqxT i0 j0 M N.
+Proof.
+move=>> /extT_rev H i j Hi Hj; specialize (H i j); simpl in H.
+erewrite 2!replaceT_correct_r in H; easy.
+Qed.
 
 Lemma replaceT_reg :
   forall {m n} i0 j0 x y A C B D (M N : 'E^{m,n}),
     replaceT i0 j0 x A B M = replaceT i0 j0 y C D N ->
-    eqxT i0 j0 M N /\ eqxF j0 A C /\ eqxF i0 B D /\ x = y.
+    x = y /\ eqxF j0 A C /\ eqxF i0 B D /\ eqxT i0 j0 M N.
 Proof.
 move=>> H; repeat split;
     [eapply replaceT_reg_l | eapply replaceT_reg_ml |
@@ -2931,43 +2931,43 @@ rewrite -> 2!replaceTc_correct_r; auto.
 Qed.
 
 Lemma replaceTr_neqxTr_compat_l :
-  forall {m n i0} A C {M N : 'E^{m,n}},
-    neqxTr i0 M N -> replaceTr i0 A M <> replaceTr i0 C N.
+  forall {m n} i0 {A C} (M N : 'E^{m,n}),
+    A <> C -> replaceTr i0 A M <> replaceTr i0 C N.
 Proof. move=>>; apply replaceF_neqxF_compat_l. Qed.
 
 Lemma replaceTr_neqxTr_compat_r :
-  forall {m n} i0 {A C} (M N : 'E^{m,n}),
-    A <> C -> replaceTr i0 A M <> replaceTr i0 C N.
+  forall {m n i0} A C {M N : 'E^{m,n}},
+    neqxTr i0 M N -> replaceTr i0 A M <> replaceTr i0 C N.
 Proof. move=>>; apply replaceF_neqxF_compat_r. Qed.
 
 Lemma replaceTr_neqxTr_reg :
   forall {m n i0 A C} {M N : 'E^{m,n}},
-    replaceTr i0 A M <> replaceTr i0 C N -> neqxTr i0 M N \/ A <> C.
+    replaceTr i0 A M <> replaceTr i0 C N -> A <> C \/ neqxTr i0 M N.
 Proof. move=>>; apply replaceF_neqxF_reg. Qed.
 
 Lemma replaceTr_neqxTr_equiv :
   forall {m n i0 A C} {M N : 'E^{m,n}},
-    replaceTr i0 A M <> replaceTr i0 C N <-> neqxTr i0 M N \/ A <> C.
+    replaceTr i0 A M <> replaceTr i0 C N <-> A <> C \/ neqxTr i0 M N.
 Proof.
 intros; split; [apply replaceTr_neqxTr_reg | intros [H | H]];
     [apply replaceTr_neqxTr_compat_l | apply replaceTr_neqxTr_compat_r]; easy.
 Qed.
 
-Lemma replaceTc_neqxTc_compat_l :
+Lemma replaceTc_neqxTc_compat_r :
   forall {m n j0} B D {M N : 'E^{m,n}},
     neqxTc j0 M N -> replaceTc j0 B M <> replaceTc j0 D N.
 Proof.
 move=>>; rewrite contra_not_r_equiv -eqxTc_not_equiv; apply replaceTc_reg.
 Qed.
 
-Lemma replaceTc_neqxTc_compat_r :
+Lemma replaceTc_neqxTc_compat_l :
   forall {m n} j0 {B D} {M N : 'E^{m,n}},
     B <> D -> replaceTc j0 B M <> replaceTc j0 D N.
 Proof. move=>>; rewrite -contra_equiv; apply replaceTc_reg. Qed.
 
 Lemma replaceTc_neqxTc_reg :
   forall {m n j0 B D} {M N : 'E^{m,n}},
-    replaceTc j0 B M <> replaceTc j0 D N -> neqxTc j0 M N \/ B <> D.
+    replaceTc j0 B M <> replaceTc j0 D N -> B <> D \/ neqxTc j0 M N.
 Proof.
 move=>>; rewrite neqxTc_not_equiv -not_and_equiv -contra_equiv.
 intros; apply replaceTc_eq; easy.
@@ -2975,18 +2975,16 @@ Qed.
 
 Lemma replaceTc_neqxTc_equiv :
   forall {m n j0 B D} {M N : 'E^{m,n}},
-    replaceTc j0 B M <> replaceTc j0 D N <-> neqxTc j0 M N \/ B <> D.
+    replaceTc j0 B M <> replaceTc j0 D N <-> B <> D \/ neqxTc j0 M N.
 Proof.
 intros; split; [apply replaceTc_neqxTc_reg | intros [H | H]];
     [apply replaceTc_neqxTc_compat_l | apply replaceTc_neqxTc_compat_r]; easy.
 Qed.
 
 Lemma replaceT_neqxT_compat_l :
-  forall {m n i0 j0} x y A C B D {M N : 'E^{m,n}},
-    neqxT i0 j0 M N -> replaceT i0 j0 x A B M <> replaceT i0 j0 y C D N.
-Proof.
-move=>>; rewrite contra_not_r_equiv -eqxT_not_equiv; apply replaceT_reg.
-Qed.
+  forall {m n} i0 j0 {x y} A C B D (M N : 'E^{m,n}),
+    x <> y -> replaceT i0 j0 x A B M <> replaceT i0 j0 y C D N.
+Proof. move=>>; rewrite -contra_equiv; apply replaceT_reg. Qed.
 
 Lemma replaceT_neqxT_compat_ml :
   forall {m n} i0 {j0} x y {A C} B D (M N : 'E^{m,n}),
@@ -3003,14 +3001,16 @@ move=>>; rewrite contra_not_r_equiv -eqxF_not_equiv; apply replaceT_reg.
 Qed.
 
 Lemma replaceT_neqxT_compat_r :
-  forall {m n} i0 j0 {x y} A C B D (M N : 'E^{m,n}),
-    x <> y -> replaceT i0 j0 x A B M <> replaceT i0 j0 y C D N.
-Proof. move=>>; rewrite -contra_equiv; apply replaceT_reg. Qed.
+  forall {m n i0 j0} x y A C B D {M N : 'E^{m,n}},
+    neqxT i0 j0 M N -> replaceT i0 j0 x A B M <> replaceT i0 j0 y C D N.
+Proof.
+move=>>; rewrite contra_not_r_equiv -eqxT_not_equiv; apply replaceT_reg.
+Qed.
 
 Lemma replaceT_neqxT_reg :
   forall {m n i0 j0 x y A C B D} {M N : 'E^{m,n}},
     replaceT i0 j0 x A B M <> replaceT i0 j0 y C D N ->
-    neqxT i0 j0 M N \/ neqxF j0 A C \/ neqxF i0 B D \/ x <> y.
+    x <> y \/ neqxF j0 A C \/ neqxF i0 B D \/ neqxT i0 j0 M N.
 Proof.
 move=>>; rewrite neqxT_not_equiv 2!neqxF_not_equiv
     -not_and4_equiv -contra_equiv.
@@ -3020,7 +3020,7 @@ Qed.
 Lemma replaceT_neqxT_equiv :
   forall {m n i0 j0 x y A C B D} {M N : 'E^{m,n}},
     replaceT i0 j0 x A B M <> replaceT i0 j0 y C D N <->
-    neqxT i0 j0 M N \/ neqxF j0 A C \/ neqxF i0 B D \/ x <> y.
+    x <> y \/ neqxF j0 A C \/ neqxF i0 B D \/ neqxT i0 j0 M N.
 Proof.
 intros; split; [apply replaceT_neqxT_reg | intros [H | [H | [H | H]]]];
     [apply replaceT_neqxT_compat_l | apply replaceT_neqxT_compat_ml |
-- 
GitLab