Issue combining naturality and implicit suspension

[wilfofford]

the following code fails to typecheck "failure", despite it being the same term as "success":

coh assoc (x(f)y(g)z(h)w) : comp (comp f g) h -> comp f (comp g h)

let assoc_then_triangle (x y z w : *) (f : x -> y) (g : y -> z) (h : z -> w) (g' : y -> w) (G : (comp g h) -> g') = comp (assoc f g h) (comp f [G])

let assoc_then_triangle_nat (x y z w : *) (f- f+ : x -> y) (f> : f- -> f+) (g : y -> z) (h : z -> w) (g' : y -> w) (G : (comp g h) -> g') = assoc_then_triangle [f>] G

let success (u v : *) (x y z w : u -> v) (f- f+ : x -> y) (f> : f- -> f+) (g : y -> z) (h : z -> w) (g' : y -> w) (G : (comp g h) -> g') = assoc_then_triangle_nat f> G

let failure (u v : *) (x y z w : u -> v) (f- f+ : x -> y) (f> : f- -> f+) (g : y -> z) (h : z -> w) (g' : y -> w) (G : (comp g h) -> g') = assoc_then_triangle [f>] G