I think I just realized a simplification to the way I've been trying to write up proof irrelevance in the canonical forms/hereditary substitution style.

Going climbing on Wednesday, all plannin'-ahead style.