Explicit Weakening

Philip Wadler

I present a novel formulation of substitution, where facts about substitution that previously required tens or hundreds of lines to justify in a proof assistant now follow immediat…