Heuristic instantiation lemma
Create a new "cached" attribute (attr_name : user_attribute hinst_lemmas). It also creates "cached" attributes for each attr_names and simp_attr_names if they have not been defined yet. Moreover, the hinst_lemmas for attr_name will be the union of the lemmas tagged with attr_name, attrs_name, and simp_attr_names. For the ones in simp_attr_names, we use the left-hand-side of the conclusion as the pattern.