Definition apstar (A:Type) (a1 a2 a3:A) (p p':a1=a2) (q q':a2=a3) : p=p' -> q=q' -> p @ q = p' @ q'. Proof. intros; apply maponpaths_12; assumption. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.