{X Y} (f : X -> Y) {a b c : X} {ab : a = b} {bc : b = c} {ac : a = c} (abc : ab @ bc = ac) : ap f ab @ ap f bc = ap f ac := (ap_pp f ab bc)^ @ ap (ap f) abc.
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.