Definition maponpaths_3 {Z Y X A : UU} (f : Z -> Y -> X -> A) {z z'} (e_z : z = z') y x : f z y x = f z' y x := maponpaths (fun z => f z y x) e_z.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.