HomeIsabelle/Phabricator

added lemmas subst_range_Var and range_vars_Var and moved stuff around