  Refinement type checkers are a powerful way to reason about functional
programs. For example, one can prove properties of a slow, specification
implementation, porting the proofs to an optimized implementation that behaves
the same. Without functional extensionality, proofs must relate functions that
are fully applied. When data itself has a higher-order representation, fully
applied proofs face serious impediments! When working with first-order data,
fully applied proofs lead to noisome duplication when using higher-order
functions.
  While dependent type theories are typically consistent with functional
extensionality axioms, refinement type systems with semantic subtyping treat
naive phrasings of functional extensionality inconsistently, leading to
unsoundness. We demonstrate this unsoundness and develop a new approach to
equality in Liquid Haskell: we define a propositional equality in a library we
call PEq. Using PEq avoids the unsoundness while still proving useful
equalities at higher types; we demonstrate its use in several case studies. We
validate PEq by building a small model and developing its metatheory.
Additionally, we prove metaproperties of PEq inside Liquid Haskell itself using
an unnamed folklore technique, which we dub `classy induction'.
