fact: Definition matcher_match {A} (m : Matcher) : forall (E: Exception) (ps : mlist (branch A (fun y => predicate_pred (matcher_pred m y)))), matcher_ret m := ltac:(destruct m as [ ? ? x]; refine x).
imports: Mtac2(Logic List intf.Unification Sorts MTele Exceptions)