fact: Definition match_eta {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.
imports: Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Contractible Basics.Equivalences Types.Prod Types.Forall Tactics.BinderApply