val from_mech =
   (1 , --`(((FromTo
                 (i)
                 (0)
                 ((arraySize(a))))
             /\
             (FromTo
                 (j)
                 (0)
                 ((arraySize(a)))))
            ==>
            (((((ArrayUpdate
                    (ArrayUpdate
                        a
                        i
                        ((a) ArrayApp (j) ))
                    j
                    ((a) ArrayApp (i) ))) ArrayApp (i) )
              =
              ((a) ArrayApp (j) ))
             /\
             ((((ArrayUpdate
                    (ArrayUpdate
                        a
                        i
                        ((a) ArrayApp (j) ))
                    j
                    ((a) ArrayApp (i) ))) ArrayApp (j) )
              =
              ((a) ArrayApp (i) ))))`-- ) ;