mtac2: better notations for goal patterns (and hypotheses binding)