1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/library_autobatch/nat/permutation".
17 include "auto/nat/compare.ma".
18 include "auto/nat/sigma_and_pi.ma".
20 definition injn: (nat \to nat) \to nat \to Prop \def
21 \lambda f:nat \to nat.\lambda n:nat.\forall i,j:nat.
22 i \le n \to j \le n \to f i = f j \to i = j.
24 theorem injn_Sn_n: \forall f:nat \to nat. \forall n:nat.
25 injn f (S n) \to injn f n.
37 theorem injective_to_injn: \forall f:nat \to nat. \forall n:nat.
38 injective nat nat f \to injn f n.
46 definition permut : (nat \to nat) \to nat \to Prop
47 \def \lambda f:nat \to nat. \lambda m:nat.
48 (\forall i:nat. i \le m \to f i \le m )\land injn f m.
50 theorem permut_O_to_eq_O: \forall h:nat \to nat.
51 permut h O \to (h O) = O.
55 apply sym_eq.autobatch.
61 theorem permut_S_to_permut: \forall f:nat \to nat. \forall m:nat.
62 permut f (S m) \to f (S m) = (S m) \to permut f m.
68 cut (f i < S m \lor f i = S m)
74 apply (not_le_Sn_n m).
89 | apply le_to_or_lt_eq.
95 | apply (injn_Sn_n f m H3)
101 definition transpose : nat \to nat \to nat \to nat \def
108 | false \Rightarrow n]].
110 notation < "(❲i↹j❳)n"
111 right associative with precedence 71
112 for @{ 'transposition $i $j $n}.
114 notation < "(❲i \atop j❳)n"
115 right associative with precedence 71
116 for @{ 'transposition $i $j $n}.
118 interpretation "natural transposition" 'transposition i j n = (transpose i j n).
120 lemma transpose_i_j_i: \forall i,j:nat. transpose i j i = j.
123 (*dopo circa 6 minuti, l'esecuzione di autobatch in questo punto non era ancora terminata*)
124 rewrite > (eqb_n_n i).autobatch.
129 lemma transpose_i_j_j: \forall i,j:nat. transpose i j j = i.
137 | rewrite > (eqb_n_n j).
144 theorem transpose_i_i: \forall i,n:nat. (transpose i i n) = n.
160 theorem transpose_i_j_j_i: \forall i,j,n:nat.
161 transpose i j n = transpose j i n.
165 [ apply (eqb_elim n j)
167 (*l'esecuzione di autobatch in questo punto, dopo circa 300 secondi, non era ancora terminata*)
177 | apply (eqb_elim n j)
179 (*simplify.reflexivity *)
181 (*simplify.reflexivity*)
186 theorem transpose_transpose: \forall i,j,n:nat.
187 (transpose i j (transpose i j n)) = n.
201 | rewrite > (eqb_n_n j).
208 | apply (eqb_elim n j)
210 rewrite > (eqb_n_n i).
218 (*l'esecuzione di autobatch in questo punto, dopo piu' di 6 minuti non era ancora terminata*)
219 rewrite > (not_eq_to_eqb_false n i H1).
220 (*l'esecuzione di autobatch in questo punto, dopo piu' alcuni minuti non era ancora terminata*)
221 rewrite > (not_eq_to_eqb_false n j H).autobatch
228 theorem injective_transpose : \forall i,j:nat.
229 injective nat nat (transpose i j).
232 (*rewrite < (transpose_transpose i j x).
233 rewrite < (transpose_transpose i j y).
238 variant inj_transpose: \forall i,j,n,m:nat.
239 transpose i j n = transpose i j m \to n = m \def
242 theorem permut_transpose: \forall i,j,n:nat. i \le n \to j \le n \to
243 permut (transpose i j) n.
250 [ (*qui autobatch non chiude il goal*)
254 [ (*aui autobatch non chiude il goal*)
257 | (*aui autobatch non chiude il goal*)
263 (*apply (injective_to_injn (transpose i j) n).
264 apply injective_transpose*)
268 theorem permut_fg: \forall f,g:nat \to nat. \forall n:nat.
269 permut f n \to permut g n \to permut (\lambda m.(f(g m))) n.
299 theorem permut_transpose_l:
300 \forall f:nat \to nat. \forall m,i,j:nat.
301 i \le m \to j \le m \to permut f m \to permut (\lambda n.transpose i j (f n)) m.
304 (*apply (permut_fg (transpose i j) f m ? ?)
305 [ apply permut_transpose;assumption
310 theorem permut_transpose_r:
311 \forall f:nat \to nat. \forall m,i,j:nat.
312 i \le m \to j \le m \to permut f m \to permut (\lambda n.f (transpose i j n)) m.
314 (*apply (permut_fg f (transpose i j) m ? ?)
316 | apply permut_transpose;assumption
320 theorem eq_transpose : \forall i,j,k,n:nat. \lnot j=i \to
321 \lnot i=k \to \lnot j=k \to
322 transpose i j n = transpose i k (transpose k j (transpose i k n)).
323 (* uffa: triplo unfold? *)
324 intros.unfold transpose.
330 rewrite > (eqb_n_n k).
332 rewrite > (not_eq_to_eqb_false j i H).
333 rewrite > (not_eq_to_eqb_false j k H2).
340 [ rewrite > (not_eq_to_eqb_false n k Hcut).
342 rewrite > (not_eq_to_eqb_false n k Hcut).
343 rewrite > (eq_to_eqb_true n j H4).
345 rewrite > (not_eq_to_eqb_false k i)
346 [ rewrite > (eqb_n_n k).
361 apply (trans_eq ? ? n)
371 rewrite > (not_eq_to_eqb_false i k H1).
372 rewrite > (not_eq_to_eqb_false i j)
374 rewrite > (eqb_n_n i).
386 rewrite > (not_eq_to_eqb_false n k H5).
387 rewrite > (not_eq_to_eqb_false n j H4).
389 rewrite > (not_eq_to_eqb_false n i H3).
390 rewrite > (not_eq_to_eqb_false n k H5).
399 theorem permut_S_to_permut_transpose: \forall f:nat \to nat.
400 \forall m:nat. permut f (S m) \to permut (\lambda n.transpose (f (S m)) (S m)
409 apply (eqb_elim (f i) (f (S m)))
413 [ apply (not_le_Sn_n m).
425 apply (eqb_elim (f i) (S m))
427 cut (f (S m) \lt (S m) \lor f (S m) = (S m))
429 [ apply le_S_S_to_le.
430 (*NB qui autobatch non chiude il goal*)
439 (*apply le_to_or_lt_eq.
444 cut (f i \lt (S m) \lor f i = (S m))
447 (*apply le_S_S_to_le.
454 | apply le_to_or_lt_eq.
469 | apply (inj_transpose (f (S m)) (S m)).
475 (* bounded bijectivity *)
477 definition bijn : (nat \to nat) \to nat \to Prop \def
478 \lambda f:nat \to nat. \lambda n. \forall m:nat. m \le n \to
479 ex nat (\lambda p. p \le n \land f p = m).
481 theorem eq_to_bijn: \forall f,g:nat\to nat. \forall n:nat.
482 (\forall i:nat. i \le n \to (f i) = (g i)) \to
483 bijn f n \to bijn g n.
488 [ apply (ex_intro ? ? a).
498 theorem bijn_Sn_n: \forall f:nat \to nat. \forall n:nat.
499 bijn f (S n) \to f (S n) = (S n) \to bijn f n.
504 apply (ex_intro ? ? a).
506 [ cut (a < S n \lor a = S n)
509 (*apply le_S_S_to_le.
512 apply (not_le_Sn_n n).
519 (*apply le_to_or_lt_eq.
530 theorem bijn_n_Sn: \forall f:nat \to nat. \forall n:nat.
531 bijn f n \to f (S n) = (S n) \to bijn f (S n).
534 cut (m < S n \lor m = S n)
538 apply (ex_intro ? ? a).
546 (*apply le_S_S_to_le.
550 (*apply (ex_intro ? ? (S n)).
558 (*apply le_to_or_lt_eq.
563 theorem bijn_fg: \forall f,g:nat\to nat. \forall n:nat.
564 bijn f n \to bijn g n \to bijn (\lambda p.f(g p)) n.
573 (*apply (ex_intro ? ? a1).
585 theorem bijn_transpose : \forall n,i,j. i \le n \to j \le n \to
586 bijn (transpose i j) n.
591 cut (m = i \lor \lnot m = i)
593 [ apply (ex_intro ? ? j).
596 | apply (eqb_elim j i)
598 (*dopo circa 360 secondi l'esecuzione di autobatch in questo punto non era ancora terminata*)
604 | rewrite > (eqb_n_n j).
612 | cut (m = j \lor \lnot m = j)
614 [ apply (ex_intro ? ? i).
617 | (*dopo circa 5 minuti, l'esecuzione di autobatch in questo punto non era ancora terminata*)
618 rewrite > (eqb_n_n i).
624 | apply (ex_intro ? ? m).
627 | rewrite > (not_eq_to_eqb_false m i)
628 [ (*dopo circa 5 minuti, l'esecuzione di autobatch in questo punto non era ancora terminata*)
629 rewrite > (not_eq_to_eqb_false m j)
639 | apply (decidable_eq_nat m j)
642 | apply (decidable_eq_nat m i)
646 theorem bijn_transpose_r: \forall f:nat\to nat.\forall n,i,j. i \le n \to j \le n \to
647 bijn f n \to bijn (\lambda p.f (transpose i j p)) n.
649 (*apply (bijn_fg f ?)
651 | apply (bijn_transpose n i j)
658 theorem bijn_transpose_l: \forall f:nat\to nat.\forall n,i,j. i \le n \to j \le n \to
659 bijn f n \to bijn (\lambda p.transpose i j (f p)) n.
662 (*apply (bijn_fg ? f)
663 [ apply (bijn_transpose n i j)
671 theorem permut_to_bijn: \forall n:nat.\forall f:nat\to nat.
672 permut f n \to bijn f n.
677 apply (ex_intro ? ? m).
680 | apply (le_n_O_elim m ? (\lambda p. f p = p))
682 | unfold permut in H.
686 (*apply le_n_O_to_eq.
691 | apply (eq_to_bijn (\lambda p.
692 (transpose (f (S n1)) (S n1)) (transpose (f (S n1)) (S n1) (f p))) f)
694 apply transpose_transpose
695 | apply (bijn_fg (transpose (f (S n1)) (S n1)))
696 [ apply bijn_transpose
697 [ unfold permut in H1.
706 (*apply permut_S_to_permut_transpose.
710 rewrite > (eqb_n_n (f (S n1))).
719 let rec invert_permut n f m \def
720 match eqb m (f n) with
725 |(S p) \Rightarrow invert_permut p f m]].
727 theorem invert_permut_f: \forall f:nat \to nat. \forall n,m:nat.
728 m \le n \to injn f n\to invert_permut n f (f m) = m.
731 [ apply (nat_case1 m)
734 (*l'applicazione di autobatch in questo punto, dopo alcuni minuti, non aveva ancora dato risultati*)
735 rewrite > (eqb_n_n (f O)).
740 (*l'applicazione di autobatch in questo punto, dopo alcuni minuti, non aveva ancora dato risultati*)
741 rewrite > (eqb_n_n (f (S m1))).
747 rewrite > (not_eq_to_eqb_false (f m) (f (S n1)))
748 [ (*l'applicazione di autobatch in questo punto, dopo parecchi secondi, non aveva ancora prodotto un risultato*)
765 apply (not_le_Sn_n n1).
773 theorem injective_invert_permut: \forall f:nat \to nat. \forall n:nat.
774 permut f n \to injn (invert_permut n f) n.
779 [ unfold bijn in Hcut.
780 generalize in match (Hcut i H1).
782 generalize in match (Hcut j H2).
791 rewrite < (invert_permut_f f n a)
792 [ rewrite < (invert_permut_f f n a1)
797 | unfold permut in H.elim H.
801 | unfold permut in H.
806 (*apply permut_to_bijn.
811 theorem permut_invert_permut: \forall f:nat \to nat. \forall n:nat.
812 permut f n \to permut (invert_permut n f) n.
820 elim (eqb i (f O));autobatch
827 elim (eqb i (f (S n1)))
838 (*apply injective_invert_permut.
843 theorem f_invert_permut: \forall f:nat \to nat. \forall n,m:nat.
844 m \le n \to permut f n\to f (invert_permut n f m) = m.
846 apply (injective_invert_permut f n H1)
847 [ unfold permut in H1.
850 cut (permut (invert_permut n f) n)
851 [ unfold permut in Hcut.
855 | apply permut_invert_permut.
856 (*NB qui autobatch non chiude il goal*)
860 | apply invert_permut_f
861 [ cut (permut (invert_permut n f) n)
862 [ unfold permut in Hcut.
868 (*apply permut_invert_permut.
871 | unfold permut in H1.
878 theorem permut_n_to_eq_n: \forall h:nat \to nat.\forall n:nat.
879 permut h n \to (\forall m:nat. m < n \to h m = m) \to h n = n.
883 cut (invert_permut n h n < n \lor invert_permut n h n = n)
885 [ rewrite < (f_invert_permut h n n) in \vdash (? ? ? %)
887 rewrite < (f_invert_permut h n n) in \vdash (? ? % ?)
892 | (*qui autobatch NON chiude il goal*)
896 | (*qui autobatch NON chiude il goal*)
899 | rewrite < H4 in \vdash (? ? % ?).
900 apply (f_invert_permut h)
902 | (*qui autobatch NON chiude il goal*)
906 | apply le_to_or_lt_eq.
907 cut (permut (invert_permut n h) n)
908 [ unfold permut in Hcut.
913 | apply permut_invert_permut.
914 (*NB aui autobatch non chiude il goal*)
920 theorem permut_n_to_le: \forall h:nat \to nat.\forall k,n:nat.
921 k \le n \to permut h n \to (\forall m:nat. m < k \to h m = m) \to
922 \forall j. k \le j \to j \le n \to k \le h j.
926 cut (h j < k \lor \not(h j < k))
930 | apply lt_to_not_le.
944 (*apply not_lt_to_le.
947 | apply (decidable_lt (h j) k)
953 let rec map_iter_i k (g:nat \to nat) f (i:nat) \def
956 | (S k) \Rightarrow f (g (S (k+i))) (map_iter_i k g f i)].
958 theorem eq_map_iter_i: \forall g1,g2:nat \to nat.
959 \forall f:nat \to nat \to nat. \forall n,i:nat.
960 (\forall m:nat. i\le m \to m \le n+i \to g1 m = g2 m) \to
961 map_iter_i n g1 f i = map_iter_i n g2 f i.
992 (* map_iter examples *)
994 theorem eq_map_iter_i_sigma: \forall g:nat \to nat. \forall n,m:nat.
995 map_iter_i n g plus m = sigma n g m.
1008 theorem eq_map_iter_i_pi: \forall g:nat \to nat. \forall n,m:nat.
1009 map_iter_i n g times m = pi n g m.
1022 theorem eq_map_iter_i_fact: \forall n:nat.
1023 map_iter_i n (\lambda m.m) times (S O) = (S n)!.
1030 (((S n1)+(S O))*(map_iter_i n1 (\lambda m.m) times (S O)) = (S(S n1))*(S n1)!).
1031 rewrite < plus_n_Sm.
1034 (*NB: qui autobatch non chiude il goal!!!*)
1040 theorem eq_map_iter_i_transpose_l : \forall f:nat\to nat \to nat.associative nat f \to
1041 symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,k:nat.
1042 map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose (k+n) (S k+n) m)) f n.
1047 fold simplify (transpose n (S n) (S n)).
1049 (*rewrite > transpose_i_j_i.
1050 rewrite > transpose_i_j_j.
1054 (f (g (S (S (m+n)))) (f (g (S (m+n))) (map_iter_i m g f n)) =
1055 f (g (transpose (S m + n) (S (S m) + n) (S (S m)+n)))
1056 (f (g (transpose (S m + n) (S (S m) + n) (S m+n)))
1057 (map_iter_i m (\lambda m1. g (transpose (S m+n) (S (S m)+n) m1)) f n))).
1058 rewrite > transpose_i_j_i.
1059 rewrite > transpose_i_j_j.
1062 rewrite < (H1 (g (S m + n))).
1064 apply eq_map_iter_i.
1068 rewrite > (not_eq_to_eqb_false m1 (S m+n))
1069 [ rewrite > (not_eq_to_eqb_false m1 (S (S m)+n))
1073 | apply (lt_to_not_eq m1 (S ((S m)+n))).
1077 change with (m1 \leq S (m+n)).
1081 | apply (lt_to_not_eq m1 (S m+n)).
1090 theorem eq_map_iter_i_transpose_i_Si : \forall f:nat\to nat \to nat.associative nat f \to
1091 symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,k,i:nat. n \le i \to i \le k+n \to
1092 map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i (S i) m)) f n.
1097 (*qui autobatch non chiude il goal*)
1098 apply (eq_map_iter_i_transpose_l f H H1 g n O)
1099 | apply antisymmetric_le
1104 | cut (i < S n1 + n \lor i = S n1 + n)
1107 (f (g (S (S n1)+n)) (map_iter_i (S n1) g f n) =
1108 f (g (transpose i (S i) (S (S n1)+n))) (map_iter_i (S n1) (\lambda m. g (transpose i (S i) m)) f n)).
1111 rewrite > (not_eq_to_eqb_false (S (S n1)+n) i)
1112 [ rewrite > (not_eq_to_eqb_false (S (S n1)+n) (S i))
1119 apply (lt_to_not_eq i (S n1+n))
1130 apply (lt_to_not_eq i (S (S n1+n)))
1141 | apply H2;autobatch
1143 | apply le_S_S_to_le.
1148 (*qui autobatch non chiude il goal*)
1149 apply (eq_map_iter_i_transpose_l f H H1 g n (S n1)).
1152 (*apply le_to_or_lt_eq.
1158 theorem eq_map_iter_i_transpose:
1159 \forall f:nat\to nat \to nat.
1160 associative nat f \to symmetric2 nat nat f \to \forall n,k,o:nat.
1161 \forall g:nat \to nat. \forall i:nat. n \le i \to S (o + i) \le S k+n \to
1162 map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i (S(o + i)) m)) f n.
1164 apply (nat_elim1 o).
1166 apply (nat_case m ?)
1168 apply (eq_map_iter_i_transpose_i_Si ? H H1);autobatch
1170 | apply le_S_S_to_le.
1174 apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g (transpose i (S(m1 + i)) m)) f n))
1180 | apply (trans_le ? (S(S (m1+i))))
1184 | (*qui autobatch non chiude il goal, chiuso invece da assumption*)
1188 | apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g
1189 (transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f n))
1190 [ (*qui autobatch dopo alcuni minuti non aveva ancora terminato la propria esecuzione*)
1191 apply (H2 O ? ? (S(m1+i)))
1197 (*apply (trans_le ? i)
1199 | change with (i \le (S m1)+i).
1202 | (*qui autobatch non chiude il goal*)
1205 | apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g
1206 (transpose i (S(m1 + i))
1207 (transpose (S(m1 + i)) (S(S(m1 + i)))
1208 (transpose i (S(m1 + i)) m)))) f n))
1209 [ (*qui autobatch dopo alcuni minuti non aveva ancora terminato la propria esecuzione*)
1215 | apply (trans_le ? (S(S (m1+i))))
1219 | (*qui autobatch NON CHIUDE il goal*)
1223 | apply eq_map_iter_i.
1230 apply (not_le_Sn_n i).
1231 rewrite < H7 in \vdash (? ? %).
1238 apply (not_le_Sn_n i).
1239 rewrite > H7 in \vdash (? ? %).
1246 (*apply (not_eq_n_Sn (S m1+i)).
1256 theorem eq_map_iter_i_transpose1: \forall f:nat\to nat \to nat.associative nat f \to
1257 symmetric2 nat nat f \to \forall n,k,i,j:nat.
1258 \forall g:nat \to nat. n \le i \to i < j \to j \le S k+n \to
1259 map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i j m)) f n.
1262 cut ((S i) < j \lor (S i) = j)
1264 [ cut (j = S ((j - (S i)) + i))
1266 apply (eq_map_iter_i_transpose f H H1 n k (j - (S i)) g i)
1271 | rewrite > plus_n_Sm.
1273 (*apply plus_minus_m_m.
1278 apply (eq_map_iter_i_transpose_i_Si f H H1 g)
1282 | apply le_S_S_to_le.
1284 (*apply (trans_le ? j)
1291 (*apply le_to_or_lt_eq.
1296 theorem eq_map_iter_i_transpose2: \forall f:nat\to nat \to nat.associative nat f \to
1297 symmetric2 nat nat f \to \forall n,k,i,j:nat.
1298 \forall g:nat \to nat. n \le i \to i \le (S k+n) \to n \le j \to j \le (S k+n) \to
1299 map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i j m)) f n.
1301 apply (nat_compare_elim i j)
1303 (*qui autobatch non chiude il goal*)
1304 apply (eq_map_iter_i_transpose1 f H H1 n k i j g H2 H6 H5)
1307 apply eq_map_iter_i.
1310 (*rewrite > (transpose_i_i j).
1313 apply (trans_eq ? ? (map_iter_i (S k) (\lambda m:nat.g (transpose j i m)) f n))
1314 [ apply (eq_map_iter_i_transpose1 f H H1 n k j i g H4 H6 H3)
1315 | apply eq_map_iter_i.
1319 apply transpose_i_j_j_i*)
1324 theorem permut_to_eq_map_iter_i:\forall f:nat\to nat \to nat.associative nat f \to
1325 symmetric2 nat nat f \to \forall k,n:nat.\forall g,h:nat \to nat.
1326 permut h (k+n) \to (\forall m:nat. m \lt n \to h m = m) \to
1327 map_iter_i k g f n = map_iter_i k (\lambda m.g(h m)) f n.
1331 rewrite > (permut_n_to_eq_n h)
1333 | (*qui autobatch non chiude il goal*)
1335 | (*qui autobatch non chiude il goal*)
1338 | apply (trans_eq ? ? (map_iter_i (S n) (\lambda m.g ((transpose (h (S n+n1)) (S n+n1)) m)) f n1))
1339 [ unfold permut in H3.
1341 apply (eq_map_iter_i_transpose2 f H H1 n1 n ? ? g)
1342 [ apply (permut_n_to_le h n1 (S n+n1))
1344 | (*qui autobatch non chiude il goal*)
1346 | (*qui autobatch non chiude il goal*)
1357 | apply (trans_eq ? ? (map_iter_i (S n) (\lambda m.
1358 (g(transpose (h (S n+n1)) (S n+n1)
1359 (transpose (h (S n+n1)) (S n+n1) (h m)))) )f n1))
1361 fold simplify (transpose (h (S n+n1)) (S n+n1) (S n+n1)).
1365 rewrite > transpose_i_j_j.
1366 rewrite > transpose_i_j_i.
1367 rewrite > transpose_i_j_j.
1369 | apply (H2 n1 (\lambda m.(g(transpose (h (S n+n1)) (S n+n1) m))))
1370 [ apply permut_S_to_permut_transpose.
1371 (*qui autobatch non chiude il goal*)
1375 rewrite > (not_eq_to_eqb_false (h m) (h (S n+n1)))
1376 [ rewrite > (not_eq_to_eqb_false (h m) (S n+n1))
1383 (*apply lt_to_not_eq.
1384 apply (trans_lt ? n1)
1394 | unfold permut in H3.
1399 apply (lt_to_not_eq m (S n+n1))
1401 (*apply (trans_lt ? n1)
1408 | unfold injn in H7.
1409 apply (H7 m (S n+n1))
1411 (*apply (trans_le ? n1)
1423 | apply eq_map_iter_i.
1426 (*rewrite > transpose_transpose.