fact: Definition idmatcher_match_invert (m : InDepMatcher) (A : Type) (y : A) (R : Prop) : R =m= idmatcher_return m -> forall (_ : Exception) (_ : mlist (branch A (fun _ => R))), R.
imports: Mtac2(Logic List intf.Unification Sorts MTele Exceptions)