simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;

renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);

specification goal: eliminated redundant Thm.legacy_freezeT -- the goal is properly declared and should always produce fixed types in the result; specification result: replaced Thm.legacy_freezeT by Thm.unvarify_global -- the final result appears to be a closed term that is globally exported;