no goals
X Y Z W : WalkingParallelPair
f : WalkingParallelPairHom X Y
g : WalkingParallelPairHom Y Z
h : WalkingParallelPairHom Z W
⊢ comp (comp f g) h = comp f (comp g h)
cases f <;> cases g <;> cases h <;> rfl