This module contains theorems to be added to the @[method_specs_simp]
simpset. When we use the
idiom of a heterogeneous class with notation (e.g. HAppend
) and a homogeneous class that the user
typically instantiates, these rewrite the method specifications generated by @[method_specs]
from
the homogeneous form to the desired heterogeneous form.
Should modules within Init
use @[method_specs]
on such instances, they should import this file.