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