make Nitpick more flexible when parsing (p)simp rules

fix soundness bug w.r.t. "Suc" with "binary_ints"

handle free variables even more gracefully; 1. show those that only occur in assumptions as part of the constants; 2. make sure locally defined Frees are given an Opt rep, just like constants generally owuld

optimize local "def"s by treating them as definitions

careful about which linear inductive predicates should be starred

help Nitpick