fact: Definition equiv_path_ind_moveL_Mp {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.
imports: HoTT(Basics Types)