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 ? : f = g by exact: funext_dep. subst g. suff : Hf = Hg by move=> ->. case: Hf => -[Hf]. case: Hg => -[Hg]. do 2 f_equal. exact: proof_irr. Qed.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)