-apply trans_eq ? ? (map_iter_i (S k) (\lambda m. g
-(transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f n).
-apply H2 O ? ? (S(m1+i)).
-simplify.apply le_S_S.apply le_O_n.
-apply trans_le ? i.assumption.
-change with i \le (S m1)+i.apply le_plus_n.
+apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g
+(transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f n)).
+apply (H2 O ? ? (S(m1+i))).
+unfold lt.apply le_S_S.apply le_O_n.
+apply (trans_le ? i).assumption.
+change with (i \le (S m1)+i).apply le_plus_n.