proposition: Lemma PathOverConstant_map1_map2 {X:Type} {x x':X} (p:x=x') {Z : Type} {z z' : Z} (q : z = z') : PathOverConstant_map2 (PathOverConstant_map1 p q) = q.
proof: Proof. now induction p. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA