Add recursive sequences to iset.mm conventions
Add recursive sequences to iset.mm conventions

This is seq3 , sum3 , iseq , and isum . Although some of the conventions
in this area may be temporary (if we are able to mostly or entirely
retire df-iseq ), seems worth documenting them anyway.

metamath/set.mm,metamath/set.mm,metamath/set.mm