fact: Definition idmatcher_match (m : InDepMatcher) : forall A y (E: Exception) (ps : mlist (branch A (fun _ => idmatcher_return m))), idmatcher_return m := ltac:(destruct m as [ ? x]; refine x).
imports: Mtac2(Logic List intf.Unification Sorts MTele Exceptions)