Skip to content

Binder_induction should handle rules that have the same K multiple times #117

Open
Open
Binder_induction should handle rules that have the same K multiple times#117
Labels
area: binder_inductionbugSomething isn't working
@jvanbruegge

Description

@jvanbruegge
jvanbruegge
opened on Nov 19, 2025

Currently, binder_induction fails if a rule as the shape x1 \notin K \rho ==> x2 \notin K \rho ==> ...

Metadata

Metadata

Assignees

No one assigned

    Labels

    area: binder_inductionbugSomething isn't working

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions