Definition maponpaths_123 {Z Y X A : UU} (f : Z -> Y -> X -> A) {z z'} (e_z : z = z') {y y'} (e_y : y = y') {x x'} (e_x : x = x') : f z y x = f z' y' x' := maponpaths_12 _ e_y e_x @ maponpaths_3 f e_z _ _.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.