Work-in-Progress: A Tactic for Pattern Matching in Autosubst

Autosubst enables automatic equality-checking up to the σ -calculus for assumption-free equalities, allowing users to avoid cumbersome reasoning about de Bruijn indices.While effective in many cases, this approach is inapplicable when matching against typing rules, reduction relations, or lemmas, requiring users to either phrase typing rules in a way that they work with Autosubst or even stating explicitly an alternative de Bruijn term.But even without β -reduction, solutions of matching may not be unique.This paper presents a work-in-progress method for automatically pattern matching against assumptions, evaluated on standard case studies including the POPLMark and POPLMark Reloaded challenges.