## Pqf.Environments

- Overview: Environments
- Connecting two kinds of multisets
- A well-founded order and tactic on multi-sets
- Multiset utilities
- Conjunction, disjunction, and implication
- A dependent version of `map`
- Tactics

## Pqf.Formulas

## Pqf.PropQuantifiers

- Overview: Propositional Quantifiers
- Definition of propositional quantifiers.
- Correctness
- Pitts' Theorem

## Pqf.SequentProps

- Overview: admissible rules in G4ip sequent calculus
- Weakening
- Inversion rules
- Contraction
- Admissibility of LJ's implication left rule
- Correctness of optimizations
- Generalized rules