Library LambdaES_Defs
Library LambdaES_fv
Library LambdaES_Infrastructure
Library LambdaES_Tactics
Library LambdaES_occ
Library LambdaJ_ndr
Library LambdaJ_Properties
Library LambdaJ_Rules
Library Metatheory_Fresh
- Tactics for fresh and notin
- Automation: hints to solve notin subgoals automatically.
- Morphisms definitions
- Tactics for fresh
Library Metatheory_Tactics
- Applying lemma modulo a simple rewriting
- Property over lists of given length
- Tactic for instantiating cofinitely quantified hypotheses
Library Metatheory
Library Metatheory_Var
- Definitions
- Basic properties on sets.
- About lists
- Properties of variables
- Dealing with list of variables
Library Rewriting_defs
This page has been generated by coqdoc