val from_mech =
   (2 , --`(((((COUNT) ((MAP (\s. 0)
                            (FILTER (\s. (((s).Id = customerId) /\ ((s).Saldo > 0)))
                                (db)))) )
              >
              0)
             ==>
             (!customer  . T ==> (((((sumOfPositiveSaldo) (customer) )) (db) )
                                  =
                                  ((((sumOfPositiveSaldo) (customer) )) (db) )) ))
            /\
            ((~((((COUNT) ((MAP (\s. 0)
                               (FILTER (\s. (((s).Id = customerId) /\ ((s).Saldo > 0)))
                                   (db)))) )
                 >
                 0)))
             ==>
             (!customer  . T ==> (((((sumOfPositiveSaldo) (customer) )) (((((deleteById) (customerId) )) (db) )) ) = ((((sumOfPositiveSaldo) (customer) )) (db) )) )))`-- ) ;