proposition: Lemma natural_fun_app_nt : naturality [the functor of S \o F] [the functor of S \o G] fun_app_nt.
proof: Proof. by move=> *; rewrite /fun_app_nt 2!FCompE -2!(@functor_o S) natural. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy