rephrase free-theorem-list-list using pointwise equality