Function rewrite_at 

pub fn rewrite_at(name: &str, occurrence: usize) -> Tactic

rewrite name (Leibniz substitution by an equality) as a tactic value. rewrite h at k as a tactic value — the k-th occurrence, 0-based.