proposition: Lemma functor_app_natural_hcomp (S F G : functor) (nt : F ~> G) : S ## nt = [the _ ~> _ of NId S] \h nt.
proof: Proof. by apply nattrans_ext => a; rewrite functor_app_naturalE. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy