strengthened datatype inversion axioms; killed a TODO in sf-lists.fst