(A:Type) := adummy : A. Ltac rewrite_refl H := match goal with | [ |- ?X ] => let dX' := eval_in ltac:(fun H' => rewrite H in H') (adummy X) in match type of dX' with | ?X' => change X' end end. Example rewrite_refl_example {A B : Type} (x : A) (f : A -> B) : ap f idpath = idpath :> (f x = f x). Proof. rewrite ap_1. reflexivity. Abort. Example rewrite_refl_example {A B : Type} (x : A) (f : A -> B) : ap f idpath = idpath :> (f x = f x). Proof. rewrite_refl @ap_1. reflexivity. Abort.
Require Import Basics.Overture Basics.PathGroupoids.