Demo for a talk given at POPL 2022.

The like-kind exchange example can be found in Prolala/Federal/Tax/Lke

The principal residence exclusion example can be found in Prolala/Federal/Tax/PrinRes.lean

The civil procedure examples are in Prolala/Federal/Civpro