proposition: Lemma nattrans_ext (f g : F ~> G) : f = g <-> forall a, (f a = g a :> (_ -> _)).
proof: Proof. split=> [ -> // |]; move: f g => [f [[Hf]]] [g [[Hg]]] /= fg''. have fg' : forall a, f a = g a :> {hom _, _} by move=> a; rewrite hom_ext fg''. move: (functional_extensionality_dep fg') => fg. by move: Hf Hg; rewrite fg=> Hf Hg; rewrite (proof_irr _ Hf Hg). Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)