fact: Fixpoint mmatch' {A P} (y : A) (ps : list (pattern t A P y)) : t (P y) := match ps with | [m:] => raise NoPatternMatches | p :: ps' => mtry' (open_pattern p) (fun e => mif unify e DoesNotMatch UniMatchNoRed then mmatch' y ps' else raise e) end.