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