Sections needed for sequent_valid

 sequent valid full sequent assignment sequent sat lemmas sequent falsification sequent satisfaction sequent rank formula list 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.