(* stuff for Wansing proof of strong normalization / cut elimination *) SN2 = SN + consts snHered :: "dertree => bool" defs snHered_def "snHered dt == set (nextUp dt) <= sn_set --> dt : sn_set" end