!_

ecc_modern/ldpc.v

@@ -820,7 +820,7 @@ Local Open Scope ring_scope.
 Local Open Scope tuple_ext_scope.
 
 Definition sumproduct_init : 'M[R]_(m, n) * 'M[R]_(m, n) :=
-  let init (x : 'F_2) := \matrix_(m0 < m, n0 < n) W `(y \__ n0 | x) in
+  let init (x : 'F_2) := \matrix_(m0 < m, n0 < n) W `(y !_ n0 | x) in
   (init 0, init 1).
 
 Definition alpha_fun (m0 : 'I_m) (n0 : 'I_n) (beta : 'M[R]_(m, n) * 'M[R]_(m, n))
@@ -830,7 +830,7 @@ Definition alpha_fun (m0 : 'I_m) (n0 : 'I_n) (beta : 'M[R]_(m, n) * 'M[R]_(m, n)
     \prod_(n1 in 'V m0 :\ n0) if t ``_ n1 == Zp0 then beta.1 m0 n1 else beta.2 m0 n1)%R.
 
 Definition beta_fun (m0 : 'I_m) (n0 : 'I_n) (x : 'F_2) (alpha : 'M[R]_(m, n)) : R :=
-  (W `(y \__ n0 | x) * \prod_(m1 in 'F n0 :\ m0) alpha m1 n0)%R.
+  (W `(y !_ n0 | x) * \prod_(m1 in 'F n0 :\ m0) alpha m1 n0)%R.
 
 Fixpoint sumproduct_loop (lmax : nat) (beta0 beta1 : 'M_(m, n)) : option ('rV['F_2]_n) :=
   match lmax with
@@ -847,7 +847,7 @@ Fixpoint sumproduct_loop (lmax : nat) (beta0 beta1 : 'M_(m, n)) : option ('rV['F
         (K * beta_fun m0 n0 x alpha)%R in
       let beta0 := \matrix_(m0 < m, n0 < n) nbeta m0 n0 0 alpha0 in
       let beta1 := \matrix_(m0 < m, n0 < n) nbeta m0 n0 1 alpha1 in
-      let estimation x n0 alpha := (W x (y \__ n0) * \prod_(m1 in 'F n0) alpha m1 n0)%R in
+      let estimation x n0 alpha := (W x (y !_ n0) * \prod_(m1 in 'F n0) alpha m1 n0)%R in
       let gamma0 n0 := estimation Zp0 n0 alpha0 in
       let gamma1 n0 := estimation Zp1 n0 alpha1 in
       let chat := \matrix_(i < 1, n0 < n) if (gamma0 n0 >= gamma1 n0)%mcR then 0 else 1 in

ecc_modern/summary.v

@@ -154,9 +154,9 @@ Lemma summary_powersetE (s : {set 'I_n}) (d : 'rV['F_2]_n) (e : 'rV['F_2]_n -> R
 Proof.
 rewrite /summary_powerset.
 transitivity (\sum_(f in {ffun 'I_n -> 'F_2} | freeon s (\row_i f i) d)
-  e (\row_(k0 < n) if k0 \in s then (fgraph f) \__ (cast_ord (esym (@card_ord n)) k0)
+  e (\row_(k0 < n) if k0 \in s then (fgraph f) !_ (cast_ord (esym (@card_ord n)) k0)
     else d ``_ k0))%R.
-  rewrite (reindex_onto (fun p => [ffun x => p \__ (cast_ord (esym (@card_ord n)) x)])
+  rewrite (reindex_onto (fun p => [ffun x => p !_ (cast_ord (esym (@card_ord n)) x)])
     (fun y => fgraph y)) /=; last first.
     move=> /= f Hf.
     apply/ffunP => /= k0.
@@ -188,7 +188,7 @@ transitivity (\sum_(f in {ffun 'I_n -> 'F_2} | freeon s (\row_i f i) d)
   by rewrite /row_of_tuple mxE tcastE.
 transitivity (\sum_(f in {ffun 'I_n -> bool} | freeon s d (\row_i F2_of_bool (f i)))
       e (\row_k0 (if k0 \in s
-                  then F2_of_bool ((fgraph f) \__ (cast_ord (esym (card_ord n)) k0))
+                  then F2_of_bool ((fgraph f) !_ (cast_ord (esym (card_ord n)) k0))
                   else d ``_ k0)))%R.
   rewrite (reindex_onto (fun f : {ffun 'I_n -> bool} => [ffun x => F2_of_bool (f x)])
     (fun f : {ffun 'I_n -> 'F_2} => [ffun x => bool_of_F2 (f x)])); last first.

information_theory/channel_coding_direct.v

@@ -286,10 +286,10 @@ Qed.
 
 (* TODO: move? *)
 Lemma rsum_rmul_tuple_pmf_tnth {C : finType} n k (Q : {fdist C}) :
-  \sum_(t : {:k.-tuple ('rV[C]_n)}) \prod_(m < k) (Q `^ n) t \__ m = 1.
+  \sum_(t : {:k.-tuple ('rV[C]_n)}) \prod_(m < k) (Q `^ n) t !_ m = 1.
 Proof.
 transitivity (\sum_(j : {ffun 'I_k -> 'rV[_]_n}) \prod_(m < k) Q `^ _ (j m)).
-  rewrite (reindex_onto (fun p => [ffun x => p\__(enum_rank x)])
+  rewrite (reindex_onto (fun p => [ffun x => p!_(enum_rank x)])
                         (fun x => fgraph x)) //=; last first.
     by move=> f _; apply/ffunP => /= i; rewrite ffunE tnth_fgraph enum_rankK.
   rewrite (big_tcast (esym (card_ord k))) esymK.
@@ -350,7 +350,7 @@ transitivity (\sum_(v : 'rV[A]_n)
   (\sum_(y in ~: [set w | prod_rV (v, w) \in `JTS P W n epsilon0])
   (W ``(| v)) y) *
     \sum_(j in {: #|M|.-1.-tuple ('rV[A]_n)})
-      (\prod_(m : M) P `^ _ ((tcast M_prednK [tuple of v :: j]) \__ (enum_rank m)))).
+      (\prod_(m : M) P `^ _ ((tcast M_prednK [tuple of v :: j]) !_ (enum_rank m)))).
   rewrite (reindex_onto (fun y : {ffun _ -> 'rV__} => \row_(i < _) y (enum_val i))
       (fun p : 'rV_ _ => [ffun x => p ``_ (enum_rank x)])) //=; last first.
     move=> v _; by apply/rowP => i; rewrite mxE ffunE enum_valK.
@@ -371,7 +371,7 @@ transitivity (\sum_(v : 'rV[A]_n)
       (\sum_(y in ~: [set y0 | prod_rV (yn, y0) \in `JTS P W n epsilon0])
       W ``(y | yn))) (\row_(i < n) a) ord0)%R.
   transitivity (\sum_(j : _)
-    (\prod_(m : M) P `^ n ((tcast M_prednK j) \__ (enum_rank m))) *
+    (\prod_(m : M) P `^ n ((tcast M_prednK j) !_ (enum_rank m))) *
       (\sum_(y in ~: [set y0 | prod_rV (nth (\row_(i < n) a) j 0, y0) \in
           `JTS P W n epsilon0])
       W ``(y | nth (\row_(i < n) a) j 0))).
@@ -384,19 +384,19 @@ transitivity (\sum_(v : 'rV[A]_n)
       by rewrite tcastE /= cast_ord_id.
     apply eq_big => m; by rewrite !inE H.
   rewrite -(@big_tuple_cons_behead _ #|M|.-1
-   (fun j => ((\prod_(m : M) P `^ n ((tcast M_prednK j) \__ (enum_rank m))) *
+   (fun j => ((\prod_(m : M) P `^ n ((tcast M_prednK j) !_ (enum_rank m))) *
      (\sum_(y in ~: [set y0 | prod_rV (nth (\row_(i < n) a) j 0, y0) \in
          `JTS P W n epsilon0]) W ``(y | nth (\row_(i < n) a) j 0)))) xpredT xpredT).
   apply eq_bigr => ta _ /=; by rewrite -big_distrl /= mulRC.
 transitivity ((\sum_(ta in 'rV[A]_n) P `^ _ ta *
     (\sum_(y in ~: [set y0 | prod_rV (ta, y0) \in `JTS P W n epsilon0])
     (W ``(| ta ) ) y)) *
-    \sum_(j in {:k.-tuple ('rV[A]_n)}) \prod_(m < k) (P `^ _ (j \__ m)))%R.
+    \sum_(j in {:k.-tuple ('rV[A]_n)}) \prod_(m < k) (P `^ _ (j !_ m)))%R.
   rewrite big_distrl /=.
   apply eq_bigr => ta _.
   rewrite -mulRA mulRCA; congr Rmult.
   transitivity (\sum_(j in {: #|'I_k|.-tuple ('rV[A]_n) })
-    P `^ _ ta * \prod_(m < k) P `^ _ (j \__ (enum_rank m)))%R.
+    P `^ _ ta * \prod_(m < k) P `^ _ (j !_ (enum_rank m)))%R.
     have k_prednK : #|'I_k.+1|.-1 = #|'I_k| by rewrite !card_ord.
     rewrite (big_tcast (esym k_prednK)) esymK.
     apply eq_bigr => i0 Hi0.
@@ -486,22 +486,22 @@ transitivity (
   \sum_(j2 in {: (#|M| - i.+1).-tuple ('rV[A]_n)})
   \sum_(j0 in 'rV[A]_n)
   \sum_(ji in 'rV[A]_n)
-  Wght.d P [ffun x => (tcast Hcast [tuple of j0 :: j1 ++ ji :: j2])\__x] *
+  Wght.d P [ffun x => (tcast Hcast [tuple of j0 :: j1 ++ ji :: j2])!_x] *
   \sum_(y | y \in [set w | prod_rV (ji, w) \in `JTS P W n epsilon0])
   (W ``(| j0)) y)%R.
   transitivity (
     \sum_(j0 in 'rV[A]_n)
     \sum_(j1 in {: i.-1.-tuple ('rV[A]_n)})
     \sum_(ji in 'rV[A]_n)
     \sum_(j2 in {: (#|M| - i.+1).-tuple ('rV[A]_n)})
-    Wght.d P [ffun x => (tcast Hcast [tuple of j0 :: j1 ++ ji :: j2])\__x] *
+    Wght.d P [ffun x => (tcast Hcast [tuple of j0 :: j1 ++ ji :: j2])!_x] *
     \sum_( y | y \in [set w | prod_rV (ji, w) \in `JTS P W n epsilon0])
     (W ``(| j0) ) y)%R.
-    rewrite (reindex_onto (fun p => [ffun x => p\__(enum_rank x)]) (fun y => fgraph y)) /=; last first.
+    rewrite (reindex_onto (fun p => [ffun x => p!_(enum_rank x)]) (fun y => fgraph y)) /=; last first.
       move=> f _; apply/ffunP => m; by rewrite ffunE tnth_fgraph enum_rankK.
     transitivity ( \sum_(j : _)
-      (Wght.d P [ffun x => j\__(enum_rank x)] *
-        Pr (W ``(| [ffun x => j\__(enum_rank x)] ord0)) (E_F_N [ffun x => j\__(enum_rank x)] i)))%R.
+      (Wght.d P [ffun x => j!_(enum_rank x)] *
+        Pr (W ``(| [ffun x => j!_(enum_rank x)] ord0)) (E_F_N [ffun x => j!_(enum_rank x)] i)))%R.
       apply eq_big => //= x; apply/eqP/eq_from_tnth => j.
       by rewrite tnth_fgraph ffunE enum_valK.
     rewrite (big_tcast (card_ord k.+1)).
@@ -524,14 +524,14 @@ transitivity (
       rewrite (reindex_onto enum_rank enum_val); last by move=> *; rewrite enum_valK.
       apply eq_big => /=; first by move=> x; rewrite enum_rankK eqxx inE.
       move=> i4 _; congr (P `^ _ _).
-      rewrite !ffunE; congr (_ \__ _).
+      rewrite !ffunE; congr (_ !_ _).
       apply/val_inj => /=.
       rewrite [LHS]eq_tcast /= !eq_tcast /= [RHS]eq_tcast eq_tcast /=; congr (_ :: _ ++ _ :: _).
       by rewrite eq_tcast.
     - apply eq_big.
       + move=> x /=.
         rewrite !inE ffunE.
-        rewrite (_ : (_ \__ _) = i2) //=.
+        rewrite (_ : (_ !_ _) = i2) //=.
         rewrite enum_rank_ord /= tcastE !cast_ord_comp (tnth_nth i0) /=.
         rewrite eq_tcast /=.
         rewrite -cat_cons nth_cat /= size_tuple prednK ?lt0n // ltnn subnn.
@@ -571,7 +571,7 @@ transitivity (
     by rewrite big_cat /= mulRC.
   rewrite [in RHS](big_nth j0) /= big_mkord.
   transitivity (\prod_(j < #|@predT M|)
-    P `^ _ ([ffun x => (tcast Hcast [tuple of j0 :: j1 ++ j3 :: j2])\__(enum_rank x)] (enum_val j)))%R.
+    P `^ _ ([ffun x => (tcast Hcast [tuple of j0 :: j1 ++ j3 :: j2])!_(enum_rank x)] (enum_val j)))%R.
     rewrite ffunE; apply eq_big => ? //= _.
     by rewrite !ffunE enum_valK.
   have j_M : (size (j1 ++ j3 :: j2)).+1 = #|M|.

information_theory/jtypes.v

@@ -553,7 +553,7 @@ rewrite size_drop size_take size_tuple -/(minn (sum_num_occ ta k.+1) n) minn_sum
 rewrite nth_drop nth_take => //.
 have Hsumk : sum_num_occ ta k + i < n by apply (leq_trans Hi (sum_num_occ_leq_n ta k.+1)).
 transitivity (enum_val k).
-  transitivity (ta\__(Ordinal Hsumk)).
+  transitivity (ta!_(Ordinal Hsumk)).
     by rewrite [in X in _ = X](tnth_nth (enum_val k)).
   apply sum_num_occ_enum_val => //=; by rewrite Hi andbT leq_addr.
 rewrite -ltn_subRL (sum_num_occ_sub ta k) in Hi.
@@ -574,7 +574,7 @@ rewrite drop_take_iota; last by rewrite sum_num_occ_inc_loc sum_num_occ_leq_n.
 apply eq_in_filter => /= i.
 rewrite mem_iota leq0n add0n /= => Hi.
 rewrite nth_zip /=; last by rewrite 2!size_tuple.
-transitivity (ta\__(Ordinal Hi) == a); by [rewrite -sum_num_occ_is_enum_val | rewrite (tnth_nth a)].
+transitivity (ta!_(Ordinal Hi) == a); by [rewrite -sum_num_occ_is_enum_val | rewrite (tnth_nth a)].
 Qed.
 
 Local Close Scope tuple_ext_scope.

lib/hamming.v

@@ -567,7 +567,7 @@ Variable n : nat.
 
 Local Open Scope tuple_ext_scope.
 Lemma card_dH (x y : n.-tuple 'F_2) :
-  (#| [pred i | y \__ i != x \__ i ] |)%N = dH (row_of_tuple x) (row_of_tuple y).
+  (#| [pred i | y !_ i != x !_ i ] |)%N = dH (row_of_tuple x) (row_of_tuple y).
 Proof.
 rewrite /dH wH_num_occ num_occ_alt /=.
 apply eq_card => /= i.
@@ -691,7 +691,7 @@ case/(_ erefl) => i [] [] H1 H2 H3.
 exists (Ordinal H1); split.
   transitivity (F2_of_bool true) => //.
   rewrite -H2 /rowF2_tuplebool (nth_map ord0); last by rewrite size_tuple.
-  rewrite (_ : _ _ _ i = (tuple_of_row x) \__ (Ordinal H1)); last first.
+  rewrite (_ : _ _ _ i = (tuple_of_row x) !_ (Ordinal H1)); last first.
     apply set_nth_default; by rewrite size_tuple.
   rewrite tnth_mktuple {1}(F2_0_1 (x ``_ (Ordinal H1))); by case: (x ``_ _ != 0%R).
 move=> j Hj.
@@ -701,7 +701,7 @@ rewrite -(H3 j) //; last first.
   by apply/Hj/val_inj.
 rewrite /rowF2_tuplebool (nth_map ord0); last by rewrite size_tuple.
 suff -> : x ``_ j = nth ord0 (tuple_of_row x) j by apply: F2_0_1.
-rewrite (_ : _ _ _ j = (tuple_of_row x) \__ j); last by rewrite tnth_mktuple.
+rewrite (_ : _ _ _ j = (tuple_of_row x) !_ j); last by rewrite tnth_mktuple.
 exact: tnth_nth.
 Qed.
 
@@ -759,13 +759,13 @@ exists (Ordinal H1), (Ordinal H3); split.
 split.
   transitivity (F2_of_bool true) => //.
   rewrite -H2 /rowF2_tuplebool (nth_map ord0); last by rewrite size_tuple.
-  rewrite (_ : _ _ _ i = (tuple_of_row x) \__ (Ordinal H1)); last first.
+  rewrite (_ : _ _ _ i = (tuple_of_row x) !_ (Ordinal H1)); last first.
     apply set_nth_default; by rewrite size_tuple.
   rewrite tnth_mktuple {1}(F2_0_1 (x ``_ (Ordinal H1))); by case: (x ``_ _ != 0%R).
 split.
   transitivity (F2_of_bool true) => //.
   rewrite -H4 /rowF2_tuplebool (nth_map ord0); last by rewrite size_tuple.
-  rewrite (_ : _ _ _ k = (tuple_of_row x) \__ (Ordinal H3)); last first.
+  rewrite (_ : _ _ _ k = (tuple_of_row x) !_ (Ordinal H3)); last first.
     apply set_nth_default; by rewrite size_tuple.
   rewrite tnth_mktuple {1}(F2_0_1 (x ``_ (Ordinal H3))); by case: (x ``_ _ != 0%R).
 move=> j ij kj.
@@ -777,7 +777,7 @@ rewrite -(H6 j) //; last first.
   by apply/ij/val_inj.
 rewrite /rowF2_tuplebool (nth_map ord0); last by rewrite size_tuple.
 suff -> : x ``_ j = nth ord0 (tuple_of_row x) j by apply: F2_0_1.
-rewrite (_ : _ _ _ j = (tuple_of_row x) \__ j); last by rewrite tnth_mktuple.
+rewrite (_ : _ _ _ j = (tuple_of_row x) !_ j); last by rewrite tnth_mktuple.
 exact: tnth_nth.
 Qed.
 

lib/num_occ.v

@@ -123,7 +123,7 @@ Proof. by rewrite /num_occ -[X in _ <= X](size_tuple t) count_size. Qed.
 
 Variables (A : finType) (n : nat) (a : A) (t : n.-tuple A).
 
-Definition set_occ := [set i | t \__ i == a].
+Definition set_occ := [set i | t !_ i == a].
 
 Lemma num_occ_alt : N(a | t) = #| set_occ |.
 Proof.
@@ -227,7 +227,7 @@ Section num_co_occ_tuple.
 
 Variables (A B : finType) (n : nat) (a : A) (b : B) (ta : n.-tuple A) (tb : n.-tuple B).
 
-Definition set_co_occ := [set i | (ta \__ i == a) && (tb \__ i == b)].
+Definition set_co_occ := [set i | (ta !_ i == a) && (tb !_ i == b)].
 
 Lemma num_co_occ_leq_n : N(a, b | ta, tb) <= n.
 Proof. rewrite /num_co_occ ; by apply num_occ_leq_n. Qed.
@@ -267,7 +267,7 @@ rewrite cover_imset.
 apply/bigcupP.
 case : ifP; last by move=> /negP H1 H ; move: H1; apply/negP; case H => {H} y0 ; rewrite 3!in_set => _ /andP [].
 rewrite in_set => /eqP Hi.
-exists (tb\__i) ; last by rewrite in_set Hi eqxx andTb.
+exists (tb!_i) ; last by rewrite in_set Hi eqxx andTb.
 rewrite in_set; apply/andP; split => //.
 apply/existsP; exists i; by rewrite in_set Hi eqxx andTb.
 Qed.
@@ -452,7 +452,7 @@ apply/andP; split; by [rewrite addnS ltnS leq_addr | rewrite ltn_add2r].
 Qed.
 
 Lemma sum_num_occ_enum_val (k : 'I_#|A|) (l : 'I_n) :
-  sum_num_occ k <= l < sum_num_occ k.+1 -> ta\__l = enum_val k.
+  sum_num_occ k <= l < sum_num_occ k.+1 -> ta!_l = enum_val k.
 Proof.
 move: (ltnSn k).
 set k':= {2}k.+1.
@@ -464,22 +464,22 @@ have : m = k by apply/eqP; rewrite eqn_leq; apply/andP.
 rewrite {Hcase} => ?; subst m.
 case/andP => [Hlm1 Hlm2].
 apply/eqP/negPn/negP; move=> abs.
-case/boolP : (lt_rank ta\__l (enum_val k)) => Hcase.
-- have Hrank : enum_rank ta\__l < k by rewrite lt_rank_alt enum_valK in Hcase.
-  have Hcontr : #|[set i | (i==l) || (sum_num_occ (enum_rank ta\__l)<= i < sum_num_occ (enum_rank ta\__l).+1)]| <= N(ta\__l|ta).
+case/boolP : (lt_rank ta!_l (enum_val k)) => Hcase.
+- have Hrank : enum_rank ta!_l < k by rewrite lt_rank_alt enum_valK in Hcase.
+  have Hcontr : #|[set i | (i==l) || (sum_num_occ (enum_rank ta!_l)<= i < sum_num_occ (enum_rank ta!_l).+1)]| <= N(ta!_l|ta).
     rewrite num_occ_alt subset_leq_card // subsetE; apply/pred0P => i /=.
     rewrite !in_set /=.
     apply/negbTE; rewrite negb_and.
-    case/boolP : (ta\__i == ta\__l) => ta_il //.
+    case/boolP : (ta!_i == ta!_l) => ta_il //.
     rewrite negb_or; apply/andP; split.
     - move: ta_il; apply contra => /eqP ->; by rewrite eqxx.
     - move: ta_il; apply contra => ta_il.
-      apply/eqP; rewrite -(enum_rankK (ta\__l)); by apply IH.
-  rewrite (_ : #|[set i | (i == l) || (sum_num_occ (enum_rank ta\__l) <= i < sum_num_occ (enum_rank ta\__l).+1)]| = N(ta\__l | ta).+1) in Hcontr; first by rewrite ltnn in Hcontr.
+      apply/eqP; rewrite -(enum_rankK (ta!_l)); by apply IH.
+  rewrite (_ : #|[set i | (i == l) || (sum_num_occ (enum_rank ta!_l) <= i < sum_num_occ (enum_rank ta!_l).+1)]| = N(ta!_l | ta).+1) in Hcontr; first by rewrite ltnn in Hcontr.
   symmetry; rewrite -addn1 sum_num_occ_rec -sum1_card.
   rewrite (bigD1 l) /=; last by rewrite in_set; apply/orP; apply or_introl.
   rewrite addnC; apply/eqP; rewrite eqn_add2l; apply/eqP.
-  transitivity (\sum_(i in [set i0 : 'I_n | nat_of_ord i0 \in iota (sum_num_occ (enum_rank ta\__l)) N(enum_val (enum_rank ta\__l) | ta)]) 1); last first.
+  transitivity (\sum_(i in [set i0 : 'I_n | nat_of_ord i0 \in iota (sum_num_occ (enum_rank ta!_l)) N(enum_val (enum_rank ta!_l) | ta)]) 1); last first.
     apply eq_bigl => i; rewrite !in_set.
     case/boolP : (i != l) => Hcase2.
     - rewrite mem_iota.
@@ -489,18 +489,18 @@ case/boolP : (lt_rank ta\__l (enum_val k)) => Hcase.
       apply/negP; case/andP => H1.
       rewrite -sum_num_occ_rec; apply/negP; rewrite -leqNgt.
       by rewrite (leq_trans _ Hlm1) // sum_num_occ_inc.
-  by rewrite sum1_card set_predleq_size enum_rankK // -{2}(enum_rankK ta\__l) -sum_num_occ_rec sum_num_occ_leq_n.
-- have {abs} {}Hcase : lt_rank (enum_val k) ta\__l.
+  by rewrite sum1_card set_predleq_size enum_rankK // -{2}(enum_rankK ta!_l) -sum_num_occ_rec sum_num_occ_leq_n.
+- have {abs} {}Hcase : lt_rank (enum_val k) ta!_l.
     rewrite lt_rank_alt; rewrite lt_rank_alt -leqNgt in Hcase.
     rewrite ltn_neqAle; apply/andP; split => //.
     rewrite enum_valK.
-    suff : k != enum_rank ta\__l by move=> ->.
+    suff : k != enum_rank ta!_l by move=> ->.
     apply/negP ; move/eqP.
     move=> abs2; symmetry in abs2; rewrite -abs2 enum_rankK {abs2} in abs.
     contradict abs ; by apply/negP/negPn/eqP.
   move/negP : (ltnn N(enum_val k | ta)) => abs; contradict abs.
   rewrite {1}num_occ_alt.
-  have H : #|[set i | ta\__i == enum_val k]| <= #|[set i : 'I_n | (sum_num_occ k <= i < l)]|.
+  have H : #|[set i | ta!_i == enum_val k]| <= #|[set i : 'I_n | (sum_num_occ k <= i < l)]|.
     apply subset_leq_card.
     rewrite subsetE; apply/pred0P => i /=.
     rewrite !in_set /=.
@@ -517,7 +517,7 @@ case/boolP : (lt_rank ta\__l (enum_val k)) => Hcase.
       have lt0m : 0 < k.
         rewrite ltnNge leqn0 ; apply/eqP => abs2.
         contradict Hcase2 ; by rewrite abs2 sum_num_occ_0 ltn0.
-      have H2 : forall (k' : 'I_#|A|) (l : 'I_n), k'.-1 < k -> l < sum_num_occ k' -> lt_rank ta\__l (enum_val k'). (* nested induction *)
+      have H2 : forall (k' : 'I_#|A|) (l : 'I_n), k'.-1 < k -> l < sum_num_occ k' -> lt_rank ta!_l (enum_val k'). (* nested induction *)
       case; elim.
       - move=> H0 l0 /= _ abs2 ; contradict abs2 ; by rewrite sum_num_occ_0 ltn0.
       - move=> k' HR' HSk l0 /= k'k Hl0.
@@ -539,18 +539,18 @@ case/boolP : (lt_rank ta\__l (enum_val k)) => Hcase.
 Qed.
 
 Lemma enum_val_sum_num_occ (k : 'I_#|A|) (l : 'I_n) :
-  ta\__l = enum_val k -> sum_num_occ k <= l < sum_num_occ k.+1.
+  ta!_l = enum_val k -> sum_num_occ k <= l < sum_num_occ k.+1.
 Proof.
 move=> Hkl; apply/negP => /negP abs.
-have : #|[set i | (i == l) || (sum_num_occ k <= i < sum_num_occ k.+1)]| <= N(ta\__l | ta).
+have : #|[set i | (i == l) || (sum_num_occ k <= i < sum_num_occ k.+1)]| <= N(ta!_l | ta).
   rewrite num_occ_alt subset_leq_card // subsetE.
   apply/pred0P => /= i /=; rewrite !in_set /=.
-  case/boolP : (ta\__i == ta\__l) => ta_il //=.
+  case/boolP : (ta!_i == ta!_l) => ta_il //=.
   apply/negbTE; rewrite negb_or; apply/andP; split.
   - move: ta_il; apply: contra => /eqP ?; subst l; by rewrite eqxx.
   - move: ta_il; apply: contra => Hsum_num_occ.
     apply/eqP; rewrite Hkl; by apply sum_num_occ_enum_val.
-suff -> : #|[set i | (i == l) || (sum_num_occ k <= i < sum_num_occ k.+1)]| = N(ta\__l | ta).+1.
+suff -> : #|[set i | (i == l) || (sum_num_occ k <= i < sum_num_occ k.+1)]| = N(ta!_l | ta).+1.
   by rewrite ltnn.
 symmetry; rewrite -addn1 sum_num_occ_rec -sum1_card.
 rewrite (bigD1 l) /=; last by rewrite in_set; apply/orP; apply or_introl.
@@ -567,7 +567,7 @@ case/boolP : (i != l) => [/negPf |] il.
 Qed.
 
 Lemma sum_num_occ_is_enum_val (k : 'I_#|A|) (l : 'I_n) :
-  sum_num_occ k <= l < sum_num_occ k.+1 = (ta\__l == enum_val k).
+  sum_num_occ k <= l < sum_num_occ k.+1 = (ta!_l == enum_val k).
 Proof.
 case/boolP : (sum_num_occ k <= l < sum_num_occ k.+1) => Hcase.
 - exact/esym/eqP/sum_num_occ_enum_val.