{A B : Type} {x1 x2 : A} {p q : x1 = x2} (r : p = q) (y : B) : transport_const p y = transport2 (fun _ => B) r y @ transport_const q y := match r with idpath => (concat_1p _)^ end.
Require Import Basics.Overture Basics.Tactics.