{X} (a b : X) (p : a = b) (P : forall (q : a = b), 1 @ p = q @ 1 -> Type) (r : P p (lrucancel 1)) : forall (q : a = b) (s : 1 @ p = q @ 1), P q s. Proof. snrapply (equiv_path_ind (fun _ => lrucancel)). exact r. Defined.
From HoTT Require Import Basics Types.