ac-math

now we can use type param in `let ... satistfy`, but still cannot use it in `instance`

some measure

use original seq_net. real seq converge iff top converge

work in progress toward measure

rename