proposition: Lemma maponpathscomp {X Y Z : UU} {x x' : X} (f : X -> Y) (g : Y -> Z) (e : x = x') : maponpaths g (maponpaths f e) = maponpaths (g ∘ f) e.
proof: Proof. intros. induction e. apply idpath. Defined.
imports: UniMath.Foundations.Preamble