Function rename_theorem 

pub fn rename_theorem(
    entry: &TheoremDecl,
    ident: &dyn Fn(&str) -> String,
    reserved: &BTreeSet<String>,
) -> (Vec<Binder>, Prop, Plan)

A theorem’s binders, proposition and proof plan with target local names.