| sequent equality | |
| sequent | |
| formula validity | |
| full assignment | |
| sat lemmas | |
| formula equality | |
| formula rank | |
| formula falsification | |
| formula satisfaction | |
| valuation | |
| formula | Propositional formula structure. |
| Kleene | Kleene 3-valued truth connectives. |
| assignment | |
| Three | Type of 3-truth-values |
| var jlc | |
| list 3 jlc | More on Lists |
| core 3 jlc | Various facts about Propositional Operators |
| discrete jlc | Basics of Discrete Types |
| bool 2 jlc | A few basic facts about asserting Bools and Bool Equalities |
| lambda jlc | Currying functions and Explicitly expressing recursion. |
| list 1 | |
| int 2 | Defines mod, floor, max and min functions over the integers. Lemmas concern basic properties of arithmetic functions over integers, and induction principles. |
| rfunction 1 | |
| prog 1 | |
| sqequal 1 | |
| quot 1 | Support lemmas for quotient type. |
| rel 1 | Common properties of binary relations. |
| union | Non canonical functions (isl, outl, outr) for union type. |
| bool 1 | Definitions, theorems and tactics for the boolean type and boolean-related expressions. |
| int 1 | Integer inequalities, subtypes, and induction lemmas for subtypes. |
| well fnd | Well-founded predicate. Rank induction lemmas and tactics. |
| fun 1 | Polymorphic identity and composition functions. Lemmas covering properties such as injectivity and surjectivity. |
| core | Some basic concepts defined type-theoretically. |