Lemma diaglemma2 {X Y : UU} (f : X -> Y) {x x' : X} (e1 : x = x') (e2 : f x' = f x) (ee : idpath (f x) = maponpaths f e1 @ e2) : maponpaths f (! e1) = e2. Proof. intros. induction e1. simpl in *. exact ee. Defined.