Updated era-sequents.txt to make the syntaxes correspond with the lispy ones in era-modules.js; to have additional parameters in some syntaxes for the subformula property; to make all dependencies on user actions explicit and on the outside; to note the nontermination of (tfa ...) with phantom types; to fix a few typos; and perhaps to do a few other things.