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