Library PropiLindep
- Independence of Instuitionistic Connectives
- Undefinability due to McKinsey
- Independence of Falsehood
- Independence of Disjunction
- Independence of Implication and Conjunction
Library PropiLmodel
- Soundness of Heyting algebra
- Completeness of Heyting algebra
- Kripke Semantics
- From Kripke to Heyting
Library PropiL
- Formulas and contexts
- Generic Entailment Relations
- Intuitionistic Gentzen System
- Intuitionistic Natural Deduction System
- Equivalence of Ni and Gi
- Intuitionistic Hilbert System Hi
- Intuitionistic Tableaux (Fitting's System)
- Decidability of Intuitionistic Gentzen
Library Base
- Base Library for ICL
- De Morgan laws
- Size recursion
- Iteration
- Decidability
- Lists
- Decidability laws for lists
- Membership
- Disjointness
- Inclusion
- Setoid rewriting with list inclusion and list equivalence
- Equivalence
- Filter
- Element removal
- Cardinality
- Duplicate-free lists
- Power lists
- Finite closure iteration
- Deprecated names, defined for backward compatibilitly
This page has been generated by coqdoc