fact: Structure Matcher {A} := MATCHER { matcher_pred: forall y, Predicate; matcher_ret: Prop; _ : forall (E: Exception) (ps : mlist (branch A (fun y => predicate_pred (matcher_pred y)))), matcher_ret }.
imports: Mtac2(Logic List intf.Unification Sorts MTele Exceptions)