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