abstraction makes a proof clearer

(the subproof is saved in a separate lemma, so we can do "Transparent weqtoforallpaths" sooner.)