pub fn induction_over(ind_type: &str, ctors: Vec<CtorSpec>) -> Tactic
induction_over (generic structural induction over ind_type) as a tactic value.
induction_over
ind_type