Tangent: `{funext_axiom:Funext}` can be removed here, and `apply funext_axiom.` below can be replaced by `apply funext.` (possibly also `apply path_forall`, though I haven't checked that one).  I was confused when I saw `funext_axiom` being called an axiom.  However, this is unrelated to this pull request, and I'll submit a separate pull request if you don't want to bother to fix that here.