TCP1_timers.lem:

==> is -->

! is forall

some definitions seem to be assertions (see _FIXME_assertion_*)

--

TCP1_params.lem:

records fields are f1:=v

duplicate field name b on sockflags; changed to b1; perhaps change fileflags instead