{T} {x y : T} (H0 : x = y) : (H0 = match H0 in (_ = y) return (x = y) with | idpath => idpath end) := match H0 with idpath => idpath end.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Contractible Basics.Equivalences. Require Import Types.Prod Types.Forall.