{A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end. Arguments {A}%_type_scope P%_function_scope {x y} p%_path_scope u : simpl nomatch. Notation "p # u" := ( _ p u) (only parsing) : path_scope. Local Lemma define_internal_paths_rew A x y P (u : P x) (H : x = y :> A) : P y. Proof. rewrite <- H. exact u. Defined.