proposition: Lemma pathOverEquations1 {X:Type} {f : X -> X} {x x' : X} (e : f x = x) (e' : f x' = x') (p : x = x') : PathOver (Y := λ x, f x = x) p e e' = ( e @ p = maponpaths f p @ e' ).
proof: Proof. induction p. simpl. apply (maponpaths (λ r, r = e')). apply pathsinv0, pathscomp0rid. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA