shouldn't `finI_from` (`filter.v`) be `open_finI_from`? (and `open_from`,`openU_from`?) `closed_bigsetU` -> `bigsetU_closed`
shouldn't
finI_from(filter.v) beopen_finI_from?(and
open_from,openU_from?)closed_bigsetU->bigsetU_closed