proposition: Lemma natural_head (phi : F ~> G) a b c (h : {hom a, b}) (f : {hom c, F a}) : [\o G # h, phi a, f] = [\o phi b, F # h, f].
proof: Proof. by rewrite -!hom_compA natural. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)