proposition: Lemma concat_p1_1 {A} {x : A} (p : x = x) (q : p = 1) : concat_p1 p @ q = ap (fun p' => p' @ 1) q.
proof: Proof. rewrite <- (inv_V q). set (r := q^). clearbody r; clear q; destruct r. reflexivity. Defined.
imports: Basics.Overture Basics.Tactics