Function by_rule 

pub fn by_rule(name: &str) -> Tactic

by_rule R as a tactic value — discharge the goal with the NAMED inference rule.