Library CoqFSetInterface
Library CoqFSetDecide
Library FSetExtra
Library FSetWeakNotin
- Implementation
- Facts about set non-membership
- Hints
- Tactics for non-membership
- Examples and test cases
Library MyFset
Library LibDefaultSimp
Library Binders
Library Syntax
Library Semantics
Library Bisimulation
- Late simulation
- Early bisimulation
- Bisimilarity
- fresh above n
- renaming
- Renaming proof itself
- Open extension
Library Struct_congr
Library Howe
Library HoweSound
This page has been generated by coqdoc