This rule is called by

-> case