{A : Type} {x y : A} (P : A -> Type) (u : P y) (p : x = y) : internal_paths_rew_r P u p = transport P p^ u. Proof. destruct p; reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Contractible Basics.Equivalences. Require Import Types.Prod Types.Forall.