General
- Existential quantifiers in Type
- Lemmas about lists in Type
- General tools
- General purpose tools in Type
- Export file for General
Syntax
Generalised Hilbert calculus iS4H
- Definition of iS4H
- iS4H captures a logic
- Properties of iS4H
- Enumeration of the language and proofs
- Lindenbaum lemma