forall mk_Account(h,a) in set rng x &
    card h > 0 and a >= 0