proposition: Lemma vassoc (F1 F2 G H : functor) (f : F1 ~> F2) (g : G ~> F1) (h : H ~> G) : f \v g \v h = f \v (g \v h).
proof: Proof. by apply/nattrans_ext => a /=; rewrite !vcompE. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy