{A} {x : A} (p : x = x) (q : p = 1) : concat_1p p @ q = ap (fun p' => 1 @ p') q. Proof. rewrite <- (inv_V q). set (r := q^). clearbody r; clear q; destruct r. reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics.