more informative spec rules: optional name;
clarified signature;
more thorough treatment of Thm.trim_context vs. Thm.transfer;