Logical constructions and theorems, beyond what has already been declared in init.datatypes and init.logic.
The command import logic does not import any axioms by default.
- connectives : the propositional connectives
- eq : additional theorems for equality and disequality
- cast : casts and heterogeneous equality
- quantifiers : existential and universal quantifiers
- identities : some useful identities
- default
Subfolders: