Definition PathOverConstant_map1_eq1 {X:Type} {x x':X} (p:x=x') {Z : Type} {z z' z'' : Z} (q: z = z') (r : z' = z'') : PathOverConstant_map1 p (q @ r) = PathOverConstant_map1 p q ⟥ r. Proof. now induction r, q. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.