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

Mathews George, Kathrin Stark

Autosubst enables automatic equality-checking up to the sigma-calculus for assumption-free equalities, allowing users to avoid cumbersome reasoning about de Bruijn indices. While e…