Module Inductive_rule.B