{T} {x : T} (E : x = x) : (match E in (_ = y) return (x = y) with | idpath => idpath end = idpath) -> idpath = E := fun H => ((H # match_eta E) ^)%path.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Contractible Basics.Equivalences. Require Import Types.Prod Types.Forall.