From 2172230a398aa39a2660d086003128c88a488894 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 08:14:41 +0100
Subject: [PATCH] Cosmetics.

---
 Subsets/Finite_family.v | 154 ++++++++++++++++++++--------------------
 Subsets/Finite_table.v  |  62 ++++++++--------
 2 files changed, 108 insertions(+), 108 deletions(-)

diff --git a/Subsets/Finite_family.v b/Subsets/Finite_family.v
index dd1ee9fc..e84b39f6 100644
--- a/Subsets/Finite_family.v
+++ b/Subsets/Finite_family.v
@@ -817,11 +817,11 @@ rewrite image_ex; apply all_not_not_ex; intros i1 Hi1; apply (Hi2 i1); easy.
 Qed.
 
 Lemma insertF_correct_l :
-  forall {n} {i0 i} x0 (A : 'E^n), i = i0 -> insertF i0 x0 A i = x0.
+  forall {n i0 i} x0 (A : 'E^n), i = i0 -> insertF i0 x0 A i = x0.
 Proof. intros; unfold insertF; destruct (ord_eq_dec _ _); easy. Qed.
 
 Lemma insertF_correct_r :
-  forall {n} {i0 i} (H : i <> i0) x0 (A : 'E^n),
+  forall {n i0 i} (H : i <> i0) x0 (A : 'E^n),
     insertF i0 x0 A i = A (insert_ord H).
 Proof.
 intros; unfold insertF; destruct (ord_eq_dec _ _); try easy.
@@ -854,7 +854,7 @@ intros; rewrite (insertF_correct_r (skip_ord_correct_m _ _))
 Qed.
 
 Lemma insert2F_correct :
-  forall {n} {i0 i1} (H : i1 <> i0) x0 x1 (A : 'E^n),
+  forall {n i0 i1} (H : i1 <> i0) x0 x1 (A : 'E^n),
     insert2F H x0 x1 A = insertF i0 x0 (insertF (insert_ord H) x1 A).
 Proof.
 move=>>; extF; unfold insert2F, insertF.
@@ -867,7 +867,7 @@ f_equal; unfold insert2_ord; apply insert_ord_compat_P.
 Qed.
 
 Lemma insert2F_equiv_def :
-  forall {n} {i0 i1} (H10 : i1 <> i0) (H01 : i0 <> i1) x0 x1 (A : 'E^n),
+  forall {n i0 i1} (H10 : i1 <> i0) (H01 : i0 <> i1) x0 x1 (A : 'E^n),
     insert2F H10 x0 x1 A = insertF i1 x1 (insertF (insert_ord H01) x0 A).
 Proof.
 intros n i0 i1 H10 H01 x0 x1 A; extF; unfold insert2F, insertF.
@@ -881,7 +881,7 @@ f_equal; apply insert2_ord_eq_sym.
 Qed.
 
 Lemma insert2F_equiv_def_alt :
-  forall {n} {i0 i1} (H : i1 <> i0) x0 x1 (A : 'E^n),
+  forall {n i0 i1} (H : i1 <> i0) x0 x1 (A : 'E^n),
     insert2F H x0 x1 A =
       insertF i1 x1 (insertF (insert_ord (not_eq_sym H)) x0 A).
 Proof. intros; apply insert2F_equiv_def. Qed.
@@ -904,50 +904,50 @@ Lemma skipF_correct_r :
 Proof. intros; unfold skipF; rewrite skip_ord_correct_r; easy. Qed.
 
 Lemma skipF_correct :
-  forall {n} {i0 i} (H : i <> i0) {A : 'E^n.+1},
+  forall {n i0 i} (H : i <> i0) {A : 'E^n.+1},
     skipF i0 A (insert_ord H) = A i.
 Proof. intros; unfold skipF; rewrite skip_insert_ord; easy. Qed.
 
 Lemma skipF_correct_alt :
-  forall {n} {i0 i j} {A : 'E^n.+1},
+  forall {n i0 i j} {A : 'E^n.+1},
     i <> i0 -> skip_ord i0 j = i -> skipF i0 A j = A i.
 Proof. move=>> H /(skip_insert_ord_eq H) ->; apply skipF_correct. Qed.
 
 Lemma skip2F_correct :
-  forall {n} {i0 i1} (H : i1 <> i0) (A : 'E^n.+2),
+  forall {n i0 i1} (H : i1 <> i0) (A : 'E^n.+2),
     skip2F H A = skipF (insert_ord H) (skipF i0 A).
 Proof. easy. Qed.
 
 Lemma skip2F_sym :
-  forall {n} {i0 i1} {H10 : i1 <> i0} (H01 : i0 <> i1) (A : 'E^n.+2),
+  forall {n i0 i1} {H10 : i1 <> i0} (H01 : i0 <> i1) (A : 'E^n.+2),
     skip2F H10 A = skip2F H01 A.
 Proof. intros; unfold skip2F; rewrite skip2_ord_sym; easy. Qed.
 
 Lemma skip2F_sym_alt :
-  forall {n} {i0 i1} {H : i1 <> i0} (A : 'E^n.+2),
+  forall {n i0 i1} {H : i1 <> i0} (A : 'E^n.+2),
     skip2F H A = skip2F (not_eq_sym H) A.
 Proof. intros; apply skip2F_sym. Qed.
 
 Lemma skip2F_equiv_def :
-  forall {n} {i0 i1} (H10 : i1 <> i0) (H01 : i0 <> i1) {A : 'E^n.+2},
+  forall {n i0 i1} (H10 : i1 <> i0) (H01 : i0 <> i1) {A : 'E^n.+2},
     skip2F H10 A = skipF (insert_ord H01) (skipF i1 A).
 Proof. intros; rewrite -(skip2F_correct); apply skip2F_sym. Qed.
 
 Lemma skip2F_equiv_def_alt :
-  forall {n} {i0 i1} (H : i1 <> i0) {A : 'E^n.+2},
+  forall {n i0 i1} (H : i1 <> i0) {A : 'E^n.+2},
     skip2F H A = skipF (insert_ord (not_eq_sym H)) (skipF i1 A).
 Proof. intros; apply skip2F_equiv_def. Qed.
 
 Lemma replaceF_correct_l :
-  forall {n} {i0 i} x0 (A : 'E^n), i = i0 -> replaceF i0 x0 A i = x0.
+  forall {n i0 i} x0 (A : 'E^n), i = i0 -> replaceF i0 x0 A i = x0.
 Proof. intros; unfold replaceF; destruct (ord_eq_dec _ _); easy. Qed.
 
 Lemma replaceF_correct_r :
-  forall {n} {i0 i} x0 (A : 'E^n), i <> i0 -> replaceF i0 x0 A i = A i.
+  forall {n i0 i} x0 (A : 'E^n), i <> i0 -> replaceF i0 x0 A i = A i.
 Proof. intros; unfold replaceF; destruct (ord_eq_dec _ _); easy. Qed.
 
 Lemma replace2F_correct_l0 :
-  forall {n} {i0 i1 i} x0 x1 (A : 'E^n),
+  forall {n i0 i1 i} x0 x1 (A : 'E^n),
     i1 <> i0 -> i = i0 -> replace2F i0 i1 x0 x1 A i = x0.
 Proof.
 intros; subst; unfold replace2F.
@@ -961,12 +961,12 @@ Lemma replace2F_correct_l1 :
 Proof. intros; unfold replace2F; apply replaceF_correct_l; easy. Qed.
 
 Lemma replace2F_correct_r :
-  forall {n} {i0 i1 i} x0 x1 (A : 'E^n),
+  forall {n i0 i1 i} x0 x1 (A : 'E^n),
     i <> i0 -> i <> i1 -> replace2F i0 i1 x0 x1 A i = A i.
 Proof. intros; unfold replace2F; rewrite -> 2!replaceF_correct_r; easy. Qed.
 
 Lemma replace2F_correct_eq :
-  forall {n} {i0 i1} x0 x1 (A : 'E^n),
+  forall {n i0 i1} x0 x1 (A : 'E^n),
     i1 = i0 -> replace2F i0 i1 x0 x1 A = replaceF i1 x1 A.
 Proof.
 intros n i0 i1 x0 x1 A H; extF i; unfold replace2F.
@@ -976,7 +976,7 @@ rewrite <- H, 3!replaceF_correct_r; easy.
 Qed.
 
 Lemma replace2F_equiv_def :
-  forall {n} {i0 i1} x0 x1 (A : 'E^n),
+  forall {n i0 i1} x0 x1 (A : 'E^n),
     i1 <> i0 -> replace2F i0 i1 x0 x1 A = replaceF i0 x0 (replaceF i1 x1 A).
 Proof.
 intros n i0 i1 x0 x1 A H; extF; unfold replace2F, replaceF.
@@ -2798,21 +2798,21 @@ rewrite concatF_correct_r; easy.
 Qed.
 
 Lemma concatF_inclF_reg_l :
-  forall {n1 n2} {PE} {A1 : 'E^n1} (A2 : 'E^n2),
+  forall {n1 n2 PE} {A1 : 'E^n1} (A2 : 'E^n2),
     inclF (concatF A1 A2) PE -> inclF A1 PE.
 Proof.
 intros n1 n2 PE A1 A2 H i1; rewrite -(firstF_concatF A1 A2); apply H.
 Qed.
 
 Lemma concatF_inclF_reg_r :
-  forall {n1 n2} {PE} (A1 : 'E^n1) {A2 : 'E^n2},
+  forall {n1 n2 PE} (A1 : 'E^n1) {A2 : 'E^n2},
     inclF (concatF A1 A2) PE -> inclF A2 PE.
 Proof.
 intros n1 n2 PE A1 A2 H i2; rewrite -(lastF_concatF A1 A2); apply H.
 Qed.
 
 Lemma concatF_inclF_equiv :
-  forall {n1 n2} {PE} (A1 : 'E^n1) (A2 : 'E^n2),
+  forall {n1 n2 PE} (A1 : 'E^n1) (A2 : 'E^n2),
     inclF (concatF A1 A2) PE <-> inclF A1 PE /\ inclF A2 PE.
 Proof.
 intros; split; intros H.
@@ -2934,7 +2934,7 @@ Context {E : Type}.
 (** Properties of operators [insertF]/[insert2F]. *)
 
 Lemma insertF_eq_gen :
-  forall {n} {i0 j0} x0 y0 (A B : 'E^n),
+  forall {n i0 j0} x0 y0 (A B : 'E^n),
     i0 = j0 -> x0 = y0 -> A = B -> insertF i0 x0 A = insertF j0 y0 B.
 Proof. intros; f_equal; easy. Qed.
 
@@ -3174,7 +3174,7 @@ rewrite -minusE; auto with zarith.
 Qed.
 
 Lemma insert2F_sym :
-  forall {n} {i0 i1} {x0 x1} {H10 : i1 <> i0} (H01 : i0 <> i1) (A : 'E^n),
+  forall {n i0 i1 x0 x1} {H10 : i1 <> i0} (H01 : i0 <> i1) (A : 'E^n),
     insert2F H10 x0 x1 A = insert2F H01 x1 x0 A.
 Proof.
 intros; rewrite insert2F_correct (insert2F_equiv_def _ _).
@@ -3182,29 +3182,29 @@ do 2 f_equal; apply insert_ord_compat_P.
 Qed.
 
 Lemma insert2F_sym_alt :
-  forall {n} {i0 i1} {H : i1 <> i0} {x0 x1} (A : 'E^n),
+  forall {n i0 i1} {H : i1 <> i0} {x0 x1} (A : 'E^n),
     insert2F H x0 x1 A = insert2F (not_eq_sym H) x1 x0 A.
 Proof. intros; apply insert2F_sym. Qed.
 
 Lemma insert2F_eq_P :
-  forall {n} {i0 i1} (H H' : i1 <> i0) x0 x1 (A : 'E^n),
+  forall {n i0 i1} (H H' : i1 <> i0) x0 x1 (A : 'E^n),
     insert2F H x0 x1 A = insert2F H' x0 x1 A.
 Proof. intros; rewrite 2!insert2F_correct insert_ord_compat_P; easy. Qed.
 
 Lemma insert2F_eq_gen :
-  forall {n} {i0 i1 j0 j1} (Hi : i1 <> i0) (Hj : j1 <> j0)
+  forall {n i0 i1 j0 j1} (Hi : i1 <> i0) (Hj : j1 <> j0)
       x0 x1 y0 y1 (A B : 'E^n),
     i0 = j0 -> i1 = j1 -> x0 = y0 -> x1 = y1 -> A = B ->
     insert2F Hi x0 x1 A = insert2F Hj y0 y1 B.
 Proof. intros; subst; apply insert2F_eq_P. Qed.
 
 Lemma insert2F_eq :
-  forall {n} {i0 i1} (H : i1 <> i0) x0 x1 y0 y1 (A B : 'E^n),
+  forall {n i0 i1} (H : i1 <> i0) x0 x1 y0 y1 (A B : 'E^n),
     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 :
-  forall {n} {i0 i1} (H : i1 <> i0) x0 x1 y0 y1 (A B : 'E^n),
+  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.
 Proof.
 move=>> H; rewrite 2!insert2F_correct in H; apply insertF_inj_l in H.
@@ -3212,14 +3212,14 @@ eapply insertF_inj_l, H.
 Qed.
 
 Lemma insert2F_inj_r0 :
-  forall {n} {i0 i1} (H : i1 <> i0) x0 x1 y0 y1 (A B : 'E^n),
+  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.
 Proof.
 move=>> H; rewrite 2!insert2F_correct in H; eapply insertF_inj_r, H.
 Qed.
 
 Lemma insert2F_inj_r1 :
-  forall {n} {i0 i1} (H : i1 <> i0) x0 x1 y0 y1 (A B : 'E^n),
+  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.
 Proof.
 move=>> H; rewrite 2!insert2F_correct in H; apply insertF_inj_l in H.
@@ -3227,7 +3227,7 @@ eapply insertF_inj_r, H.
 Qed.
 
 Lemma insert2F_inj :
-  forall {n} {i0 i1} (H : i1 <> i0) x0 x1 y0 y1 (A B : 'E^n),
+  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.
 Proof.
 move=>> H; repeat split;
@@ -3236,29 +3236,29 @@ move=>> H; repeat split;
 Qed.
 
 Lemma insert2F_nextF_compat_l :
-  forall {n} {i0 i1} (H : i1 <> i0) x0 x1 y0 y1 {A B : 'E^n},
+  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 :
-  forall {n} {i0 i1} (H : i1 <> i0) {x0} x1 {y0} y1 (A B : 'E^n),
+  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.
 
 Lemma insert2F_nextF_compat_r1 :
-  forall {n} {i0 i1} (H : i1 <> i0) x0 {x1} y0 {y1} (A B : 'E^n),
+  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.
 
 Lemma insert2F_nextF_reg :
-  forall {n} {i0 i1} (H : i1 <> i0) {x0 x1 y0 y1} {A B : 'E^n},
+  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.
 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},
+  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.
 Proof.
 intros; split; [apply insert2F_nextF_reg | intros [H1 | [H1 | H1]]];
@@ -3339,25 +3339,25 @@ Lemma eqxF_equiv :
 Proof. intros; split. intros; apply skipF_eq; easy. apply skipF_reg. Qed.
 
 Lemma skipF_neqxF_compat :
-  forall {n} {i0} {A B : 'E^n.+1}, neqxF i0 A B -> skipF i0 A <> skipF i0 B.
+  forall {n i0} {A B : 'E^n.+1}, neqxF i0 A B -> skipF i0 A <> skipF i0 B.
 Proof.
 move=>>; rewrite contra_not_r_equiv -eqxF_not_equiv; apply skipF_reg.
 Qed.
 
 Lemma skipF_neqxF_reg :
-  forall {n} {i0} {A B : 'E^n.+1}, skipF i0 A <> skipF i0 B -> neqxF i0 A B.
+  forall {n i0} {A B : 'E^n.+1}, skipF i0 A <> skipF i0 B -> neqxF i0 A B.
 Proof.
 move=>>; rewrite contra_not_l_equiv -eqxF_not_equiv eqxF_equiv; easy.
 Qed.
 
 Lemma neqxF_equiv :
-  forall {n} {i0} {A B : 'E^n.+1}, neqxF i0 A B <-> skipF i0 A <> skipF i0 B.
+  forall {n i0} {A B : 'E^n.+1}, neqxF i0 A B <-> skipF i0 A <> skipF i0 B.
 Proof.
 intros; split. intros; apply skipF_neqxF_compat; easy. apply skipF_neqxF_reg.
 Qed.
 
 Lemma PAF_ind_skipF :
-  forall {n} {i0} {P : 'Prop^n.+1}, P i0 -> PAF (skipF i0 P) -> PAF P.
+  forall {n i0} {P : 'Prop^n.+1}, P i0 -> PAF (skipF i0 P) -> PAF P.
 Proof.
 intros n i0 P H0 H1 i; destruct (ord_eq_dec i i0) as [-> | Hi]; [easy |].
 rewrite -(skip_insert_ord Hi); apply H1.
@@ -3630,7 +3630,7 @@ apply liftF_S_reg; try rewrite liftF_S_insertF_0; easy.
 Qed.
 
 Lemma insertF_skipF_comm :
-  forall {n} {j0 j1 i0 i1} x1 (A : 'E^n.+1),
+  forall {n j0 j1 i0 i1} x1 (A : 'E^n.+1),
     i0 = skip_ord i1 j0 -> i1 = skip_ord i0 j1 ->
     insertF j1 x1 (skipF j0 A) = skipF i0 (insertF i1 x1 A).
 Proof.
@@ -3643,7 +3643,7 @@ rewrite (skip_insert_ord_gen _ _ _ Hi0 Hi1); easy.
 Qed.
 
 Lemma skipF_insertF_comm :
-  forall {n} {i0 i1} (Hi : i1 <> i0) x0 (A : 'E^n.+1),
+  forall {n i0 i1} (Hi : i1 <> i0) x0 (A : 'E^n.+1),
     let j1 := insert_ord Hi in
     let j0 := insert_ord (not_eq_sym Hi) in
     skipF i1 (insertF i0 x0 A) = insertF j0 x0 (skipF j1 A).
@@ -3677,16 +3677,16 @@ Lemma skipF_last : forall {n} (A : 'E^n.+1), skipFmax A = widenF_S A.
 Proof. intros; extF; apply skipF_correct_l; apply /ltP; easy. Qed.
 
 Lemma skipF_0 :
-  forall {n} {i0} {A : 'E^n.+2}, i0 <> ord0 -> skipF i0 A ord0 = A ord0.
+  forall {n i0} {A : 'E^n.+2}, i0 <> ord0 -> skipF i0 A ord0 = A ord0.
 Proof. intros; apply skipF_correct_alt; [| apply skip_ord_0]; easy. Qed.
 
 Lemma skipF_max :
-  forall {n} {i0} {A : 'E^n.+2},
+  forall {n i0} {A : 'E^n.+2},
     i0 <> ord_max -> skipF i0 A ord_max = A ord_max.
 Proof. intros; apply skipF_correct_alt; [| apply skip_ord_max]; easy. Qed.
 
 Lemma skip2F_eq_P :
-  forall {n} {i0 i1} {H : i1 <> i0} (H' : i1 <> i0) (A : 'E^n.+2),
+  forall {n i0 i1} {H : i1 <> i0} (H' : i1 <> i0) (A : 'E^n.+2),
     skip2F H A = skip2F H' A.
 Proof. intros; unfold skip2F; rewrite skip2_ord_compat_P; easy. Qed.
 
@@ -3710,7 +3710,7 @@ contradict Hj1; apply (skip_ord_inj i0); rewrite skip_insert_ord; easy.
 Qed.
 
 Lemma skip2F_eq_gen :
-  forall {n} {i0 i1 j0 j1} (Hi : i1 <> i0) (Hj : j1 <> j0) (A B : 'E^n.+2),
+  forall {n i0 i1 j0 j1} (Hi : i1 <> i0) (Hj : j1 <> j0) (A B : 'E^n.+2),
     i0 = j0 -> i1 = j1 -> eqx2F i0 i1 A B -> skip2F Hi A = skip2F Hj B.
 Proof.
 intros n i0 i1 j0 j1 Hi Hj A B Hi0 Hi1 H; subst j0 j1.
@@ -3725,38 +3725,38 @@ apply skip2F_eq_lt; easy.
 Qed.
 
 Lemma skip2F_eq :
-  forall {n} {i0 i1} (H : i1 <> i0) (A B : 'E^n.+2),
+  forall {n i0 i1} (H : i1 <> i0) (A B : 'E^n.+2),
     eqx2F i0 i1 A B -> skip2F H A = skip2F H B.
 Proof. intros; apply skip2F_eq_gen; easy. Qed.
 
 Lemma skip2F_reg :
-  forall {n} {i0 i1} (H : i1 <> i0) (A B : 'E^n.+2),
+  forall {n i0 i1} (H : i1 <> i0) (A B : 'E^n.+2),
     skip2F H A = skip2F H B -> eqx2F i0 i1 A B.
 Proof.
 move=>> /extF_rev H i [H0 H1]; rewrite -(skip2_insert2_ord _ H0 H1); apply H.
 Qed.
 
 Lemma eqx2F_equiv :
-  forall {n} {i0 i1} (H : i1 <> i0) (A B : 'E^n.+2),
+  forall {n i0 i1} (H : i1 <> i0) (A B : 'E^n.+2),
     eqx2F i0 i1 A B <-> skip2F H A = skip2F H B.
 Proof. intros; split. intros; apply skip2F_eq; easy. apply skip2F_reg. Qed.
 
 Lemma skip2F_neqx2F_compat :
-  forall {n} {i0 i1} (H : i1 <> i0) (A B : 'E^n.+2),
+  forall {n i0 i1} (H : i1 <> i0) (A B : 'E^n.+2),
     neqx2F i0 i1 A B -> skip2F H A <> skip2F H B.
 Proof.
 move=>>; rewrite contra_not_r_equiv -eqx2F_not_equiv; apply skip2F_reg.
 Qed.
 
 Lemma skip2F_neqx2F_reg :
-  forall {n} {i0 i1} (H : i1 <> i0) (A B : 'E^n.+2),
+  forall {n i0 i1} (H : i1 <> i0) (A B : 'E^n.+2),
     skip2F H A <> skip2F H B -> neqx2F i0 i1 A B.
 Proof.
 move=>>; rewrite contra_not_l_equiv -eqx2F_not_equiv -eqx2F_equiv; easy.
 Qed.
 
 Lemma neqx2F_equiv :
-  forall {n} {i0 i1} (H : i1 <> i0) (A B : 'E^n.+2),
+  forall {n i0 i1} (H : i1 <> i0) (A B : 'E^n.+2),
     neqx2F i0 i1 A B <-> skip2F H A <> skip2F H B.
 Proof.
 intros; split;
@@ -3790,7 +3790,7 @@ rewrite (insert_ord_correct_r _ ord_lt_1_max) lower_S_correct;
 Qed.
 
 Lemma PAF_ind_skip2F :
-  forall {n} {i0 i1} (H : i1 <> i0) {P : 'Prop^n.+2},
+  forall {n i0 i1} (H : i1 <> i0) {P : 'Prop^n.+2},
     P i0 -> P i1 -> PAF (skip2F H P) -> PAF P.
 Proof.
 intros n i0 i1 Hi P H0 H1 H2; rewrite skip2F_correct in H2.
@@ -3799,19 +3799,19 @@ apply: (PAF_ind_skipF H0) (PAF_ind_skipF H1 H2).
 Qed.
 
 Lemma extF_skip2F :
-  forall {n} {i0 i1} (H : i1 <> i0) (A B : 'E^n.+2),
+  forall {n i0 i1} (H : i1 <> i0) (A B : 'E^n.+2),
     A i0 = B i0 -> A i1 = B i1 -> skip2F H A = skip2F H B -> A = B.
 Proof. move=>>; rewrite -eqx2F_equiv; apply eqx2F_reg. Qed.
 
 Lemma skip2F_insert2F :
-  forall {n} {i0 i1} (H : i1 <> i0) x0 x1 (A : 'E^n),
+  forall {n i0 i1} (H : i1 <> i0) x0 x1 (A : 'E^n),
     skip2F H (insert2F H x0 x1 A) = A.
 Proof.
 intros; rewrite skip2F_correct insert2F_correct 2!skipF_insertF; easy.
 Qed.
 
 Lemma insert2F_skip2F :
-  forall {n} {i0 i1} (H : i1 <> i0) (A : 'E^n.+2),
+  forall {n i0 i1} (H : i1 <> i0) (A : 'E^n.+2),
     insert2F H (A i0) (A i1) (skip2F H A) = A.
 Proof.
 intros n i0 i1 H A.
@@ -3898,7 +3898,7 @@ Lemma replaceF_eq :
 Proof. intros; apply replaceF_eq_gen; easy. Qed.
 
 Lemma replaceF_reg_l :
-  forall {n} {i0 x0 y0} {A B : 'E^n},
+  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.
@@ -3906,7 +3906,7 @@ erewrite 2!replaceF_correct_r in H; easy.
 Qed.
 
 Lemma replaceF_reg_r :
-  forall {n} {i0 x0 y0} (A B : 'E^n),
+  forall {n i0 x0 y0} (A B : 'E^n),
     replaceF i0 x0 A = replaceF i0 y0 B -> x0 = y0.
 Proof.
 move=> n i0 x0 y0 A B /extF_rev H; specialize (H i0); simpl in H.
@@ -3914,7 +3914,7 @@ erewrite 2!replaceF_correct_l in H; easy.
 Qed.
 
 Lemma replaceF_reg :
-  forall {n} {i0 x0 y0} {A B : 'E^n},
+  forall {n i0 x0 y0} {A B : 'E^n},
     replaceF i0 x0 A = replaceF i0 y0 B -> eqxF i0 A B /\ x0 = y0.
 Proof.
 move=>> H; split; [eapply replaceF_reg_l | eapply replaceF_reg_r]; apply H.
@@ -3932,7 +3932,7 @@ rewrite -> 2!replaceF_correct_r; auto.
 Qed.
 
 Lemma replaceF_neqxF_compat_l :
-  forall {n} {i0} x0 y0 {A B : 'E^n},
+  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.
 
@@ -3942,7 +3942,7 @@ Lemma replaceF_neqxF_compat_r :
 Proof. move=>>; rewrite -contra_equiv; apply replaceF_reg. Qed.
 
 Lemma replaceF_neqxF_reg :
-  forall {n} {i0 x0 y0} {A B : 'E^n},
+  forall {n i0 x0 y0} {A B : 'E^n},
     replaceF i0 x0 A <> replaceF i0 y0 B -> neqxF i0 A B \/ x0 <> y0.
 Proof.
 move=>>; rewrite neqxF_not_equiv -not_and_equiv -contra_equiv.
@@ -3950,7 +3950,7 @@ intros; apply replaceF_eq; easy.
 Qed.
 
 Lemma replaceF_neqxF_equiv :
-  forall {n} {i0 x0 y0} {A B : 'E^n},
+  forall {n i0 x0 y0} {A B : 'E^n},
     replaceF i0 x0 A <> replaceF i0 y0 B <-> neqxF i0 A B \/ x0 <> y0.
 Proof.
 intros; split; [apply replaceF_neqxF_reg | intros [H | H]];
@@ -4023,7 +4023,7 @@ rewrite -> tripleF_2, replaceF_correct_l; easy.
 Qed.
 
 Lemma PAF_ind_replaceF :
-  forall {n} {i0} p0 {P : 'Prop^n}, P i0 -> PAF (replaceF i0 p0 P) -> PAF P.
+  forall {n i0} p0 {P : 'Prop^n}, P i0 -> PAF (replaceF i0 p0 P) -> PAF P.
 Proof.
 intros n i0 p0 P H0 H1 i; destruct (ord_eq_dec i i0) as [-> | Hi]; [easy |].
 rewrite -(replaceF_correct_r p0 _ Hi); easy.
@@ -4043,7 +4043,7 @@ Lemma skipF_replaceF :
 Proof. move=>>; apply skipF_eq; move=>> H; apply replaceF_correct_r; easy. Qed.
 
 Lemma replace2F_sym :
-  forall {n} {i0 i1} x0 x1 (A : 'E^n),
+  forall {n i0 i1} x0 x1 (A : 'E^n),
     i1 <> i0 -> replace2F i0 i1 x0 x1 A = replace2F i1 i0 x1 x0 A.
 Proof. move=>>; apply replace2F_equiv_def. Qed.
 
@@ -4072,7 +4072,7 @@ erewrite 2!replaceF_correct_r in H1; easy.
 Qed.
 
 Lemma replace2F_reg_r0 :
-  forall {n} {i0 i1} x0 x1 y0 y1 (A B : 'E^n),
+  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.
@@ -4084,7 +4084,7 @@ Lemma replace2F_reg_r1 :
 Proof. move=>>; apply replaceF_reg_r. Qed.
 
 Lemma replace2F_reg :
-  forall {n} {i0 i1} x0 x1 y0 y1 (A B : 'E^n),
+  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.
 Proof.
@@ -4093,14 +4093,14 @@ move=>> Hi; repeat split; [eapply replace2F_reg_l |
 Qed.
 
 Lemma replace2F_neqxF_compat_l :
-  forall {n} {i0 i1} x0 x1 y0 y1 {A B : 'E^n},
+  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_l.
 Qed.
 
 Lemma replace2F_neqxF_compat_r0 :
-  forall {n} {i0 i1} {x0} x1 {y0} y1 (A B : 'E^n),
+  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.
 
@@ -4110,7 +4110,7 @@ Lemma replace2F_neqxF_compat_r1 :
 Proof. move=>>; rewrite -contra_equiv; apply replace2F_reg_r1. Qed.
 
 Lemma replace2F_neqxF_reg :
-  forall {n} {x0 x1 y0 y1 i0 i1} {A B : 'E^n},
+  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.
 Proof.
@@ -4119,7 +4119,7 @@ intros; apply replace2F_eq; easy.
 Qed.
 
 Lemma replace2F_neqxF_equiv :
-  forall {n} {i0 i1} {x0 x1 y0 y1} {A B : 'E^n},
+  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.
 Proof.
@@ -4161,7 +4161,7 @@ intros; unfold replace2F; rewrite replaceF_tripleF_1 replaceF_tripleF_2; easy.
 Qed.
 
 Lemma PAF_ind_replace2F :
-  forall {n} {i0 i1} p0 p1 {P : 'Prop^n},
+  forall {n i0 i1} p0 p1 {P : 'Prop^n},
     P i0 -> P i1 -> PAF (replace2F i0 i1 p0 p1 P) -> PAF P.
 Proof.
 intros n i0 i1 p0 p1 P H0 H1 H2; destruct (ord_eq_dec i1 i0) as [Hi | Hi].
@@ -4183,7 +4183,7 @@ rewrite -(replace2F_correct_r x0 x1 A Hi0 Hi1)
 Qed.
 
 Lemma skip2F_replace2F :
-  forall {n} {i0 i1} (H : i1 <> i0) x0 x1 (A : 'E^n.+2),
+  forall {n i0 i1} (H : i1 <> i0) x0 x1 (A : 'E^n.+2),
     skip2F H (replace2F i0 i1 x0 x1 A) = skip2F H A.
 Proof.
 intros; apply skip2F_eq; move=>> [H0 H1]; apply replace2F_correct_r; easy.
@@ -4235,17 +4235,17 @@ move=>> [q Hq1 Hq2]; apply (Bijective (permutF_can Hq2) (permutF_can Hq1)).
 Qed.
 
 Lemma permutF_inj_compat :
-  forall {n} {p} (Hp : injective p) {A : 'E^n},
+  forall {n p} (Hp : injective p) {A : 'E^n},
     injective A -> injective (permutF p A).
 Proof. move=>> Hp A HA i j /HA /Hp; easy. Qed.
 
 Lemma permutF_f_inv_l :
-  forall {n} {p} (Hp : bijective p) (A : 'E^n),
+  forall {n p} (Hp : bijective p) (A : 'E^n),
     A = permutF (f_inv Hp) (permutF p A).
 Proof. intros n p Hp A; rewrite permutF_can //; apply f_inv_can_r. Qed.
 
 Lemma permutF_f_inv_r :
-  forall {n} {p} (Hp : bijective p) (A : 'E^n),
+  forall {n p} (Hp : bijective p) (A : 'E^n),
     A = permutF p (permutF (f_inv Hp) A).
 Proof. intros n p Hp A; rewrite permutF_can //; apply f_inv_can_l. Qed.
 
@@ -4292,7 +4292,7 @@ Lemma lastF_permutF :
 Proof. easy. Qed.
 
 Lemma skipF_permutF :
-  forall {n} {p} (Hp : injective p) i0 (A : 'E^n.+1),
+  forall {n p} (Hp : injective p) i0 (A : 'E^n.+1),
     skipF i0 (permutF p A) = permutF (skip_f_ord Hp i0) (skipF (p i0) A).
 Proof. move=>>; extF; unfold permutF; rewrite skipF_correct; easy. Qed.
 
@@ -5031,7 +5031,7 @@ Lemma filterPF_lastF :
 Proof. intros; rewrite filterPF_splitF castF_can lastF_concatF; easy. Qed.
 
 Lemma lenPF_permutF :
-  forall {n} {p} {P : 'Prop^n}, injective p -> lenPF (permutF p P) = lenPF P.
+  forall {n p} {P : 'Prop^n}, injective p -> lenPF (permutF p P) = lenPF P.
 Proof.
 intros [| n] p P Hp; [rewrite !lenPF_nil; easy |].
 apply (bijS_eq_card p), (injS_surjS_bijS I_S_nonempty);
diff --git a/Subsets/Finite_table.v b/Subsets/Finite_table.v
index b3eca1b0..5d636bfc 100644
--- a/Subsets/Finite_table.v
+++ b/Subsets/Finite_table.v
@@ -735,26 +735,26 @@ Lemma liftT_S_equiv_def :
 Proof. easy. Qed.
 
 Lemma insertTr_correct_l :
-  forall {m n} {i0 i} A (M : 'E^{m,n}), i = i0 -> insertTr i0 A M i = A.
+  forall {m n i0 i} A (M : 'E^{m,n}), i = i0 -> insertTr i0 A M i = A.
 Proof. intros; apply insertF_correct_l; easy. Qed.
 
 Lemma insertTr_correct_r :
-  forall {m n} {i0 i} (H : i <> i0) A (M : 'E^{m,n}),
+  forall {m n i0 i} (H : i <> i0) A (M : 'E^{m,n}),
     insertTr i0 A M i = M (insert_ord H).
 Proof. intros; apply insertF_correct_r; easy. Qed.
 
 Lemma insertTc_correct_l :
-  forall {m n} {j0 j} i B (M : 'E^{m,n}),
+  forall {m n j0 j} i B (M : 'E^{m,n}),
     j = j0 -> insertTc j0 B M i j = B i.
 Proof. intros; apply insertF_correct_l; easy. Qed.
 
 Lemma insertTc_correct_r :
-  forall {m n} {j0 j} (H : j <> j0) i B (M : 'E^{m,n}),
+  forall {m n j0 j} (H : j <> j0) i B (M : 'E^{m,n}),
     insertTc j0 B M i j = M i (insert_ord H).
 Proof. intros; apply insertF_correct_r; easy. Qed.
 
 Lemma insertT_correct_lr :
-  forall {m n} {i0 i} j0 x A B (M : 'E^{m,n}),
+  forall {m n i0 i} j0 x A B (M : 'E^{m,n}),
     i = i0 -> insertT i0 j0 x A B M i = insertF j0 x A.
 Proof. move=>>; apply insertTr_correct_l. Qed.
 
@@ -769,7 +769,7 @@ rewrite insertTr_correct_r insertF_correct_r insertTc_correct_l; easy.
 Qed.
 
 Lemma insertT_correct_r :
-  forall {m n} {i0 i} (Hi : i <> i0) {j0 j} (Hj : j <> j0) x A B (M : 'E^{m,n}),
+  forall {m n i0 i} (Hi : i <> i0) {j0 j} (Hj : j <> j0) x A B (M : 'E^{m,n}),
     insertT i0 j0 x A B M i j = M (insert_ord Hi) (insert_ord Hj).
 Proof.
 intros; unfold insertT; rewrite insertTr_correct_r insertTc_correct_r; easy.
@@ -871,25 +871,25 @@ Lemma skipT_equiv_def :
 Proof. easy. Qed.
 
 Lemma replaceTr_correct_l :
-  forall {m n} {i0 i} A (M : 'E^{m,n}), i = i0 -> replaceTr i0 A M i = A.
+  forall {m n i0 i} A (M : 'E^{m,n}), i = i0 -> replaceTr i0 A M i = A.
 Proof. move=>>; apply replaceF_correct_l. Qed.
 
 Lemma replaceTr_correct_r :
-  forall {m n} {i0 i} A (M : 'E^{m,n}), i <> i0 -> replaceTr i0 A M i = M i.
+  forall {m n i0 i} A (M : 'E^{m,n}), i <> i0 -> replaceTr i0 A M i = M i.
 Proof. move=>>; apply replaceF_correct_r. Qed.
 
 Lemma replaceTc_correct_l :
-  forall {m n} {j0 j} i B (M : 'E^{m,n}),
+  forall {m n j0 j} i B (M : 'E^{m,n}),
     j = j0 -> replaceTc j0 B M i j = B i.
 Proof. move=>>; apply replaceF_correct_l. Qed.
 
 Lemma replaceTc_correct_r :
-  forall {m n} {j0 j} i B (M : 'E^{m,n}),
+  forall {m n j0 j} i B (M : 'E^{m,n}),
     j <> j0 -> replaceTc j0 B M i j = M i j.
 Proof. move=>>; apply replaceF_correct_r. Qed.
 
 Lemma replaceT_correct_lr :
-  forall {m n} {i0 i} j0 x A B (M : 'E^{m,n}),
+  forall {m n i0 i} j0 x A B (M : 'E^{m,n}),
     i = i0 -> replaceT i0 j0 x A B M i = replaceF j0 x A.
 Proof. move=>>; apply replaceTr_correct_l. Qed.
 
@@ -904,7 +904,7 @@ rewrite -> replaceTr_correct_r, replaceF_correct_r, replaceTc_correct_l; easy.
 Qed.
 
 Lemma replaceT_correct_r :
-  forall {m n} {i0 i j0 j} x A B (M : 'E^{m,n}),
+  forall {m n i0 i j0 j} x A B (M : 'E^{m,n}),
     i <> i0 -> j <> j0 -> replaceT i0 j0 x A B M i j = M i j.
 Proof.
 intros; unfold replaceT;
@@ -2449,50 +2449,50 @@ Lemma eqxT_equiv :
 Proof. intros; split. intros; apply skipT_eq; easy. apply skipT_reg. Qed.
 
 Lemma skipTr_neqxTr_compat :
-  forall {m n} {i0} {M N : 'E^{m.+1,n}},
+  forall {m n i0} {M N : 'E^{m.+1,n}},
     neqxTr i0 M N -> skipTr i0 M <> skipTr i0 N.
 Proof. move=>>; apply skipF_neqxF_compat. Qed.
 
 Lemma skipTr_neqxTr_reg :
-  forall {m n} {i0} {M N : 'E^{m.+1,n}},
+  forall {m n i0} {M N : 'E^{m.+1,n}},
     skipTr i0 M <> skipTr i0 N -> neqxTr i0 M N.
 Proof. move=>>; apply skipF_neqxF_reg. Qed.
 
 Lemma skipTc_neqxTc_compat :
-  forall {m n} {j0} {M N : 'E^{m,n.+1}},
+  forall {m n j0} {M N : 'E^{m,n.+1}},
     neqxTc j0 M N -> skipTc j0 M <> skipTc j0 N.
 Proof.
 move=>>; rewrite contra_not_r_equiv -eqxTc_not_equiv; apply skipTc_reg.
 Qed.
 
 Lemma skipTc_neqxTc_reg :
-  forall {m n} {j0} {M N : 'E^{m,n.+1}},
+  forall {m n j0} {M N : 'E^{m,n.+1}},
     skipTc j0 M <> skipTc j0 N -> neqxTc j0 M N.
 Proof.
 move=>>; rewrite contra_not_l_equiv -eqxTc_not_equiv; apply skipTc_eq.
 Qed.
 
 Lemma skipT_neqxT_compat :
-  forall {m n} {i0 j0} {M N : 'E^{m.+1,n.+1}},
+  forall {m n i0 j0} {M N : 'E^{m.+1,n.+1}},
     neqxT i0 j0 M N -> skipT i0 j0 M <> skipT i0 j0 N.
 Proof.
 move=>>; rewrite contra_not_r_equiv -eqxT_not_equiv; apply skipT_reg.
 Qed.
 
 Lemma skipT_neqxT_reg :
-  forall {m n} {i0 j0} {M N : 'E^{m.+1,n.+1}},
+  forall {m n i0 j0} {M N : 'E^{m.+1,n.+1}},
     skipT i0 j0 M <> skipT i0 j0 N -> neqxT i0 j0 M N.
 Proof.
 move=>>; rewrite contra_not_l_equiv -eqxT_not_equiv eqxT_equiv; easy.
 Qed.
 
 Lemma neqxTr_equiv :
-  forall {m n} {i0} {M N : 'E^{m.+1,n}},
+  forall {m n i0} {M N : 'E^{m.+1,n}},
     neqxTr i0 M N <-> skipTr i0 M <> skipTr i0 N.
 Proof. move=>>; apply neqxF_equiv. Qed.
 
 Lemma neqxTc_equiv :
-  forall {m n} {j0} {M N : 'E^{m,n.+1}},
+  forall {m n j0} {M N : 'E^{m,n.+1}},
     neqxTc j0 M N <-> skipTc j0 M <> skipTc j0 N.
 Proof.
 intros; split;
@@ -2500,7 +2500,7 @@ intros; split;
 Qed.
 
 Lemma neqxT_equiv :
-  forall {m n} {i0 j0} {M N : 'E^{m.+1,n.+1}},
+  forall {m n i0 j0} {M N : 'E^{m.+1,n.+1}},
     neqxT i0 j0 M N <-> skipT i0 j0 M <> skipT i0 j0 N.
 Proof.
 intros; split;
@@ -2931,7 +2931,7 @@ rewrite -> 2!replaceTc_correct_r; auto.
 Qed.
 
 Lemma replaceTr_neqxTr_compat_l :
-  forall {m n} {i0} A C {M N : 'E^{m,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_l. Qed.
 
@@ -2941,12 +2941,12 @@ Lemma replaceTr_neqxTr_compat_r :
 Proof. move=>>; apply replaceF_neqxF_compat_r. Qed.
 
 Lemma replaceTr_neqxTr_reg :
-  forall {m n} {i0 A C} {M N : 'E^{m,n}},
+  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.
 Proof. move=>>; apply replaceF_neqxF_reg. Qed.
 
 Lemma replaceTr_neqxTr_equiv :
-  forall {m n} {i0 A C} {M N : 'E^{m,n}},
+  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.
 Proof.
 intros; split; [apply replaceTr_neqxTr_reg | intros [H | H]];
@@ -2954,7 +2954,7 @@ intros; split; [apply replaceTr_neqxTr_reg | intros [H | H]];
 Qed.
 
 Lemma replaceTc_neqxTc_compat_l :
-  forall {m n} {j0} B D {M N : 'E^{m,n}},
+  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.
@@ -2966,7 +2966,7 @@ Lemma replaceTc_neqxTc_compat_r :
 Proof. move=>>; rewrite -contra_equiv; apply replaceTc_reg. Qed.
 
 Lemma replaceTc_neqxTc_reg :
-  forall {m n} {j0 B D} {M N : 'E^{m,n}},
+  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.
 Proof.
 move=>>; rewrite neqxTc_not_equiv -not_and_equiv -contra_equiv.
@@ -2974,7 +2974,7 @@ intros; apply replaceTc_eq; easy.
 Qed.
 
 Lemma replaceTc_neqxTc_equiv :
-  forall {m n} {j0 B D} {M N : 'E^{m,n}},
+  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.
 Proof.
 intros; split; [apply replaceTc_neqxTc_reg | intros [H | H]];
@@ -2982,7 +2982,7 @@ intros; split; [apply replaceTc_neqxTc_reg | intros [H | H]];
 Qed.
 
 Lemma replaceT_neqxT_compat_l :
-  forall {m n} {i0 j0} x y A C B D {M N : 'E^{m,n}},
+  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.
@@ -2996,7 +2996,7 @@ move=>>; rewrite contra_not_r_equiv -eqxF_not_equiv; apply replaceT_reg.
 Qed.
 
 Lemma replaceT_neqxT_compat_mr :
-  forall {m n} {i0} j0 x y A C {B D} (M N : 'E^{m,n}),
+  forall {m n i0} j0 x y A C {B D} (M N : 'E^{m,n}),
     neqxF i0 B D -> replaceT i0 j0 x A B M <> replaceT i0 j0 y C D N.
 Proof.
 move=>>; rewrite contra_not_r_equiv -eqxF_not_equiv; apply replaceT_reg.
@@ -3008,7 +3008,7 @@ Lemma replaceT_neqxT_compat_r :
 Proof. move=>>; rewrite -contra_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}},
+  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.
 Proof.
@@ -3018,7 +3018,7 @@ intros; apply replaceT_eq; easy.
 Qed.
 
 Lemma replaceT_neqxT_equiv :
-  forall {m n} {i0 j0 x y A C B D} {M N : 'E^{m,n}},
+  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.
 Proof.
-- 
GitLab