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