Function rewrite_hyp_at 

pub fn rewrite_hyp_at(eq: &str, hyp: &str, occurrence: usize) -> Tactic

rewrite h at hp — the LOCATION form, rewriting a HYPOTHESIS rather than the goal.